Union axiom

Can form the union of a set

The set whose existence is asserted here is unique by (Ext)
We denote this by
(formally, we are introducing a unary operation symbol to the language of ZF)
So is the union of the members of

We write for

Intersection

We can prove

Indeed, start with a nonempty set and form the set

using (Un) and (Sep). Technically, we work in a model here and then we deduce the sentence above by Gödel’s Completeness Theorem for First-Order Logic

The unique set constructed here is denoted by
We write for

We can now define the domain of a Function
If , then since
we have
So we can form the set

using (Un) and (Sep)

Formally, we introduce a unary operation symbol
Note that this is defined for any set but it only has a meaning for functions.