Axiom ax-un

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

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vy	|- y
1		vz	|- z
2		vw	|- w
3	1	cv	|- z
4	2	cv	|- w
5	3 4	wcel	|- z e. w
6		vx	|- x
7	6	cv	|- x
8	4 7	wcel	|- w e. x
9	5 8	wa	|- ( z e. w /\ w e. x )
10	9 2	wex	|- E. w ( z e. w /\ w e. x )
11	0	cv	|- y
12	3 11	wcel	|- z e. y
13	10 12	wi	|- ( E. w ( z e. w /\ w e. x ) -> z e. y )
14	13 1	wal	|- A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
15	14 0	wex	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )