all x { some p { all y { y ⊆ x then y ∈ p }}}
You're probably wondering why "then" isn't "iff" in the above formula. We assert some p that contains all the subsets of x. You can always restrict p to the subsets of x by comprehension, thus giving the power set. You'll see this in some of the other axioms. We assert the existence of a set with certain members, and you can always cut it down to precisely those members later.
all x,y { some u { x ∈ u and y ∈ u }}
Set x = y above, and u is the set containing x. Thus we have ∅, the set containing ∅, the set containing the set containing ∅, and so on.
The pair u = (x,y) is the unordered pair. The ordered pair can be built by pairing (x) with (x,y). This generalizes to n-tuples, as described in the section on relations.
all x { some u { all z { z ∈ u if some y { z ∈ y and y ∈ x }}}}
For any x and y, let w be the pair (x,y) and take the union over w to get the union of x and y. Repeating this process, all finite unions of sets are sets.
Restrict the union over the set x to only those elements that belong to every member of x, and you have the intersection over x. By pairing sets together, the finite intersection of sets is another set.
At this point we have enough axioms to build the cross product of x and y. First let p be the power set of x∪y. Then let q be the power set of p. Now q contains sets like ((a),(a,b)). By comprehension, force the members of q to have one or two elements. If w ∈ q and w has one element, make sure this element is a set containing a, for some a in x. If w ∈ q and w has two elements, make sure those elements are a set containing a for some a in x and a set containing a and b where b comes from y. Thus q has been restricted to the cross product of x and y. The cross product of any two sets, or finitely many sets, is another set.
Further applications of comprehension restrict the cross product to any describable relation or function. These relations are all sets.
If the set r is a relation, restrict to the members with one element, then take the union across these members. Take the union of this set to find the domain of the relation. A similar, though somewhat more complicated procedure extracts the range.
Let the set r be an equivalence relation. Let d be the domain union the range, and let p be the power set of d. Now restrict p to those subsets where every pair in the subset appears in the relation. This gives the set of equivalence classes. Cross d with p and restrict to give a function that maps each member of the domain into its equivalence class.
Finally, we would like to establish the direct product of an indexed set of sets. If every x ∈ S has an associated set Ax, let U be the union over all the sets Ax. Let C be the cross product of S with U. Restrict C to the ordered pairs that map each x to something in Ax. Let F be the power set of C and restrict F so that each member of F is a function on all of S. That builds the direct product across S, as a set.
Is there anything in the direct product, or is it the empty set? That depends on the axiom of choice.