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.