Axiom ax-un 2861

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

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

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 953	. . . . . . 7 class z
3		vw	. . . . . . . 8 set w
4	3	cv 953	. . . . . . 7 class w
5	2, 4	wcel 956	. . . . . 6 wff z ∈ w
6		vx	. . . . . . . 8 set x
7	6	cv 953	. . . . . . 7 class x
8	4, 7	wcel 956	. . . . . 6 wff w ∈ x
9	5, 8	wa 223	. . . . 5 wff (z ∈ w ⋀ w ∈ x)
10	9, 3	wex 978	. . . 4 wff ∃w(z ∈ w ⋀ w ∈ x)
11		vy	. . . . . 6 set y
12	11	cv 953	. . . . 5 class y
13	2, 12	wcel 956	. . . 4 wff z ∈ y
14	10, 13	wi 3	. . 3 wff (∃w(z ∈ w ⋀ w ∈ x) → z ∈ y)
15	14, 1	wal 952	. 2 wff ∀z(∃w(z ∈ w ⋀ w ∈ x) → z ∈ y)
16	15, 11	wex 978	1 wff ∃y∀z(∃w(z ∈ w ⋀ w ∈ x) → z ∈ y)

This axiom is referenced by:  axun 2862  axun2 2863

Copyright terms: Public domain