Axiom ax-un 1076

Description: Axiom of Union. An axiom of Zermelo-Fraenkel set theory. It states that the union of any set exists. A variant is Axiom Union of [BellMachover] p. 466 (which can be derived from this version using bm1.3ii 1481). A version using abbreviations is uniex 1947.

Assertion

Ref	Expression
ax-un	⊢ ∃y∀z(∃w(z ∈ w ∧ w ∈ x) → z ∈ y)

Distinct variable group(s):   x,y,z,w

Detailed syntax breakdown of Axiom ax-un

Step	Hyp	Ref	Expression
1		vz	. . . . . . 7 set z
2		vw	. . . . . . 7 set w
3	1, 2	wel 803	. . . . . 6 wff z ∈ w
4		vx	. . . . . . 7 set x
5	2, 4	wel 803	. . . . . 6 wff w ∈ x
6	3, 5	wa 196	. . . . 5 wff (z ∈ w ∧ w ∈ x)
7	6, 2	wex 678	. . . 4 wff ∃w(z ∈ w ∧ w ∈ x)
8		vy	. . . . 5 set y
9	1, 8	wel 803	. . . 4 wff z ∈ y
10	7, 9	wi 2	. . 3 wff (∃w(z ∈ w ∧ w ∈ x) → z ∈ y)
11	10, 1	wal 672	. 2 wff ∀z(∃w(z ∈ w ∧ w ∈ x) → z ∈ y)
12	11, 8	wex 678	1 wff ∃y∀z(∃w(z ∈ w ∧ w ∈ x) → z ∈ y)

This axiom is referenced by:  axun 1081

metamath.org