Axiom ax-un 2866

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

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

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 955	. . . . . . 7 class z
3		vw	. . . . . . . 8 set w
4	3	cv 955	. . . . . . 7 class w
5	2, 4	wcel 958	. . . . . 6 wff z e. w
6		vx	. . . . . . . 8 set x
7	6	cv 955	. . . . . . 7 class x
8	4, 7	wcel 958	. . . . . 6 wff w e. x
9	5, 8	wa 223	. . . . 5 wff (z e. w /\ w e. x)
10	9, 3	wex 980	. . . 4 wff E.w(z e. w /\ w e. x)
11		vy	. . . . . 6 set y
12	11	cv 955	. . . . 5 class y
13	2, 12	wcel 958	. . . 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 954	. 2 wff A.z(E.w(z e. w /\ w e. x) -> z e. y)
16	15, 11	wex 980	1 wff E.yA.z(E.w(z e. w /\ w e. x) -> z e. y)

This axiom is referenced by:  axun 2867  axun2 2868

Copyright terms: Public domain