HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Axiom ax-un 3929
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 3931 states that the union itself exists. A version with the standard abbreviation for union is uniex2 3932. A version using class notation is uniex 3933.

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

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
StepHypRef Expression
1 vz . . . . . . . 8 set z
21cv 1585 . . . . . . 7 class z
3 vw . . . . . . . 8 set w
43cv 1585 . . . . . . 7 class w
52, 4wcel 1588 . . . . . 6 wff z e. w
6 vx . . . . . . . 8 set x
76cv 1585 . . . . . . 7 class x
84, 7wcel 1588 . . . . . 6 wff w e. x
95, 8wa 337 . . . . 5 wff (z e. w /\ w e. x)
109, 3wex 1615 . . . 4 wff E.w(z e. w /\ w e. x)
11 vy . . . . . 6 set y
1211cv 1585 . . . . 5 class y
132, 12wcel 1588 . . . 4 wff z e. y
1410, 13wi 3 . . 3 wff (E.w(z e. w /\ w e. x) -> z e. y)
1514, 1wal 1584 . 2 wff A.z(E.w(z e. w /\ w e. x) -> z e. y)
1615, 11wex 1615 1 wff E.yA.z(E.w(z e. w /\ w e. x) -> z e. y)
Colors of variables: wff set class
This axiom is referenced by:  zfun 3930  axun2 3931
Copyright terms: Public domain