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	|- E.yA.z(E.w(z e. w /\ w e. x) -> z e. 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 e. w
4		vx	. . . . . . 7 set x
5	2, 4	wel 803	. . . . . 6 wff w e. x
6	3, 5	wa 196	. . . . 5 wff (z e. w /\ w e. x)
7	6, 2	wex 678	. . . 4 wff E.w(z e. w /\ w e. x)
8		vy	. . . . 5 set y
9	1, 8	wel 803	. . . 4 wff z e. y
10	7, 9	wi 2	. . 3 wff (E.w(z e. w /\ w e. x) -> z e. y)
11	10, 1	wal 672	. 2 wff A.z(E.w(z e. w /\ w e. x) -> z e. y)
12	11, 8	wex 678	1 wff E.yA.z(E.w(z e. w /\ w e. x) -> z e. y)

This axiom is referenced by:  axun 1081

metamath.org