Axiom ax-un 3929

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

The union of a class df-uni 3367 should not be confused with the union of two classes df-un 2832. Their relationship is shown in unipr 3380.

Assertion

Ref	Expression
ax-un	|- E.yA.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	. . . . . . . 8 set z
2	1	cv 1585	. . . . . . 7 class z
3		vw	. . . . . . . 8 set w
4	3	cv 1585	. . . . . . 7 class w
5	2, 4	wcel 1588	. . . . . 6 wff z e. w
6		vx	. . . . . . . 8 set x
7	6	cv 1585	. . . . . . 7 class x
8	4, 7	wcel 1588	. . . . . 6 wff w e. x
9	5, 8	wa 337	. . . . 5 wff (z e. w /\ w e. x)
10	9, 3	wex 1615	. . . 4 wff E.w(z e. w /\ w e. x)
11		vy	. . . . . 6 set y
12	11	cv 1585	. . . . 5 class y
13	2, 12	wcel 1588	. . . 4 wff z e. y
14	10, 13	wi 3	. . 3 wff (E.w(z e. w /\ w e. x) -> z e. y)
15	14, 1	wal 1584	. 2 wff A.z(E.w(z e. w /\ w e. x) -> z e. y)
16	15, 11	wex 1615	1 wff E.yA.z(E.w(z e. w /\ w e. x) -> z e. y)

This axiom is referenced by:  zfun 3930  axun2 3931

Copyright terms: Public domain