Description: Axiom of Union. An axiom of Zermelo-Fraenkel set theory. It states that a set y exists that includes the union of a given set x i.e. the collection of all members of the members of x . The variant axun2 states that the union itself exists. A version with the standard abbreviation for union is uniex2 . A version using class notation is uniex .
The union of a class df-uni should not be confused with the union of two classes df-un . Their relationship is shown in unipr . (Contributed by NM, 23-Dec-1993)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-un | ⊢ ∃ 𝑦 ∀ 𝑧 ( ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vy | ⊢ 𝑦 | |
| 1 | vz | ⊢ 𝑧 | |
| 2 | vw | ⊢ 𝑤 | |
| 3 | 1 | cv | ⊢ 𝑧 |
| 4 | 2 | cv | ⊢ 𝑤 |
| 5 | 3 4 | wcel | ⊢ 𝑧 ∈ 𝑤 |
| 6 | vx | ⊢ 𝑥 | |
| 7 | 6 | cv | ⊢ 𝑥 |
| 8 | 4 7 | wcel | ⊢ 𝑤 ∈ 𝑥 |
| 9 | 5 8 | wa | ⊢ ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) |
| 10 | 9 2 | wex | ⊢ ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) |
| 11 | 0 | cv | ⊢ 𝑦 |
| 12 | 3 11 | wcel | ⊢ 𝑧 ∈ 𝑦 |
| 13 | 10 12 | wi | ⊢ ( ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) |
| 14 | 13 1 | wal | ⊢ ∀ 𝑧 ( ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) |
| 15 | 14 0 | wex | ⊢ ∃ 𝑦 ∀ 𝑧 ( ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) |