# 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 ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\exists {w}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\wedge {w}\in {x}\right)\to {z}\in {y}\right)$

### 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}\in {w}$
6 vx ${setvar}{x}$
7 6 cv ${setvar}{x}$
8 4 7 wcel ${wff}{w}\in {x}$
9 5 8 wa ${wff}\left({z}\in {w}\wedge {w}\in {x}\right)$
10 9 2 wex ${wff}\exists {w}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\wedge {w}\in {x}\right)$
11 0 cv ${setvar}{y}$
12 3 11 wcel ${wff}{z}\in {y}$
13 10 12 wi ${wff}\left(\exists {w}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\wedge {w}\in {x}\right)\to {z}\in {y}\right)$
14 13 1 wal ${wff}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\exists {w}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\wedge {w}\in {x}\right)\to {z}\in {y}\right)$
15 14 0 wex ${wff}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\exists {w}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\wedge {w}\in {x}\right)\to {z}\in {y}\right)$