Axiom ax-un 2922

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

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

Assertion

Ref	Expression
ax-un	⊢ ∃y∀z(∃w(z ∈ w ⋀ w ∈ x) → z ∈ 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 996	. . . . . . 7 class z
3		vw	. . . . . . . 8 set w
4	3	cv 996	. . . . . . 7 class w
5	2, 4	wcel 999	. . . . . 6 wff z ∈ w
6		vx	. . . . . . . 8 set x
7	6	cv 996	. . . . . . 7 class x
8	4, 7	wcel 999	. . . . . 6 wff w ∈ x
9	5, 8	wa 230	. . . . 5 wff (z ∈ w ⋀ w ∈ x)
10	9, 3	wex 1021	. . . 4 wff ∃w(z ∈ w ⋀ w ∈ x)
11		vy	. . . . . 6 set y
12	11	cv 996	. . . . 5 class y
13	2, 12	wcel 999	. . . 4 wff z ∈ y
14	10, 13	wi 3	. . 3 wff (∃w(z ∈ w ⋀ w ∈ x) → z ∈ y)
15	14, 1	wal 995	. 2 wff ∀z(∃w(z ∈ w ⋀ w ∈ x) → z ∈ y)
16	15, 11	wex 1021	1 wff ∃y∀z(∃w(z ∈ w ⋀ w ∈ x) → z ∈ y)

This axiom is referenced by:  axun 2923  axun2 2924

Copyright terms: Public domain