Metamath Proof Explorer

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 y z w z w w x z y

Detailed syntax breakdown

Step Hyp Ref Expression
0 vy setvar y
1 vz setvar z
2 vw setvar w
3 1 cv setvar z
4 2 cv setvar w
5 3 4 wcel wff z w
6 vx setvar x
7 6 cv setvar x
8 4 7 wcel wff w x
9 5 8 wa wff z w w x
10 9 2 wex wff w z w w x
11 0 cv setvar y
12 3 11 wcel wff z y
13 10 12 wi wff w z w w x z y
14 13 1 wal wff z w z w w x z y
15 14 0 wex wff y z w z w w x z y