Axiom ax-un 6949

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 6951 states that the union itself exists. A version with the standard abbreviation for union is uniex2 6952. A version using class notation is uniex 6953.

The union of a class df-uni 4437 should not be confused with the union of two classes df-un 3579. Their relationship is shown in unipr 4449. (Contributed by NM, 23-Dec-1993.)

Assertion

Ref	Expression
ax-un	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )

Distinct variable group:   x, w, y, z

Detailed syntax breakdown of Axiom ax-un

Step	Hyp	Ref	Expression
1		vz	. . . . . . 7 setvar z
2		vw	. . . . . . 7 setvar w
3	1, 2	wel 1991	. . . . . 6 wff z e. w
4		vx	. . . . . . 7 setvar x
5	2, 4	wel 1991	. . . . . 6 wff w e. x
6	3, 5	wa 384	. . . . 5 wff ( z e. w /\ w e. x )
7	6, 2	wex 1704	. . . 4 wff E. w ( z e. w /\ w e. x )
8		vy	. . . . 5 setvar y
9	1, 8	wel 1991	. . . 4 wff z e. y
10	7, 9	wi 4	. . 3 wff ( E. w ( z e. w /\ w e. x ) -> z e. y )
11	10, 1	wal 1481	. 2 wff A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
12	11, 8	wex 1704	1 wff E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )

This axiom is referenced by:  zfun  6950  axun2  6951