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.