Can take a subset of a set. This is an axiom scheme

where is a formula with
The set whose existence is asserted by (Sep) is unique by (Ext)
We denote this by
Formally, we are introducing an -arry operation symbol to the language.