Axiom of separation for $n$ tuples or $n$ place predicates The axiom of separation seems to only work when you are using an arity 1 type predicate, how then can we form relations? I know the power axiom allows for you to work with a set of subsets and in turn this is how we can define ordered pairs, however I do not see how this can be used in conjunction with the separation axiom to define sets by a binary predicate. It would seem as tho all you can say when trying to form a binary predicate is $\{x:x \subseteq D\}$ (where $x$ is an ordered pair and $D$ is the power set of some domain $D_0$) and there is no way to add in a predicate with 2 variables to this since the separation axiom only guarantees subsets formed with arity 1 predicates. So is there some generalized axiom of separation I am unaware of? How else does a binary predicate form it's own subset?
 A: The ordinary axiom of separation works fine for that too.
If our ordered pairs follow Kuratowski's definition $\langle x,y\rangle = \{\{x\},\{x,y\}\}$, then $A\times A\subseteq \mathcal P(\mathcal P(A))$, and therefore we can view
$$ \{ \langle x,y\rangle \in A\times A \mid \varphi(x,y) \} $$
as an abbreviation for
$$ \{ z \in \mathcal P(\mathcal P(A)) \mid \underbrace{\exists x,y: z=\langle x,y\rangle \land x\in A \land y\in A \land \varphi(x,y)}_{\text{a one-position predicate in the variable }z} \} $$
A: The thing about pairs, or ordered triplets, or whatever, is that those are objects in the universe that we can "identify" via a definable property. Moreover, we can extract each coordinate from them if necessary.
So there is a formula $\varphi(x,y)$ which is true if and only if $x$ is an ordered $42$-tuple, and $y$ is the element in the 33th coordinate.
Given an $n$-ary relation, you just need to write the correct formula using some fixed encoding of $n$-tuples and "decoding" for each coordinate; then you can just use the usual separation/replacement/collections schemata.
