# Metamath Proof Explorer

## Definition df-gzun

Description: The Godel-set version of the Axiom of Unions. (Contributed by Mario Carneiro, 14-Jul-2013)

Ref Expression
Assertion df-gzun ${⊢}\mathrm{AxUn}=\left[{\exists }_{𝑔}{1}_{𝑜}\left[{\forall }_{𝑔}{2}_{𝑜}\left(\left[{\exists }_{𝑔}{1}_{𝑜}\left(\left({2}_{𝑜}{\in }_{𝑔}{1}_{𝑜}\right){\wedge }_{𝑔}\left({1}_{𝑜}{\in }_{𝑔}\varnothing \right)\right)\right]{\to }_{𝑔}\left({2}_{𝑜}{\in }_{𝑔}{1}_{𝑜}\right)\right)\right]\right]$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cgzu ${class}\mathrm{AxUn}$
1 c1o ${class}{1}_{𝑜}$
2 c2o ${class}{2}_{𝑜}$
3 cgoe ${class}{\in }_{𝑔}$
4 2 1 3 co ${class}\left({2}_{𝑜}{\in }_{𝑔}{1}_{𝑜}\right)$
5 cgoa ${class}{\wedge }_{𝑔}$
6 c0 ${class}\varnothing$
7 1 6 3 co ${class}\left({1}_{𝑜}{\in }_{𝑔}\varnothing \right)$
8 4 7 5 co ${class}\left(\left({2}_{𝑜}{\in }_{𝑔}{1}_{𝑜}\right){\wedge }_{𝑔}\left({1}_{𝑜}{\in }_{𝑔}\varnothing \right)\right)$
9 8 1 cgox ${class}\left[{\exists }_{𝑔}{1}_{𝑜}\left(\left({2}_{𝑜}{\in }_{𝑔}{1}_{𝑜}\right){\wedge }_{𝑔}\left({1}_{𝑜}{\in }_{𝑔}\varnothing \right)\right)\right]$
10 cgoi ${class}{\to }_{𝑔}$
11 9 4 10 co ${class}\left(\left[{\exists }_{𝑔}{1}_{𝑜}\left(\left({2}_{𝑜}{\in }_{𝑔}{1}_{𝑜}\right){\wedge }_{𝑔}\left({1}_{𝑜}{\in }_{𝑔}\varnothing \right)\right)\right]{\to }_{𝑔}\left({2}_{𝑜}{\in }_{𝑔}{1}_{𝑜}\right)\right)$
12 11 2 cgol ${class}\left[{\forall }_{𝑔}{2}_{𝑜}\left(\left[{\exists }_{𝑔}{1}_{𝑜}\left(\left({2}_{𝑜}{\in }_{𝑔}{1}_{𝑜}\right){\wedge }_{𝑔}\left({1}_{𝑜}{\in }_{𝑔}\varnothing \right)\right)\right]{\to }_{𝑔}\left({2}_{𝑜}{\in }_{𝑔}{1}_{𝑜}\right)\right)\right]$
13 12 1 cgox ${class}\left[{\exists }_{𝑔}{1}_{𝑜}\left[{\forall }_{𝑔}{2}_{𝑜}\left(\left[{\exists }_{𝑔}{1}_{𝑜}\left(\left({2}_{𝑜}{\in }_{𝑔}{1}_{𝑜}\right){\wedge }_{𝑔}\left({1}_{𝑜}{\in }_{𝑔}\varnothing \right)\right)\right]{\to }_{𝑔}\left({2}_{𝑜}{\in }_{𝑔}{1}_{𝑜}\right)\right)\right]\right]$
14 0 13 wceq ${wff}\mathrm{AxUn}=\left[{\exists }_{𝑔}{1}_{𝑜}\left[{\forall }_{𝑔}{2}_{𝑜}\left(\left[{\exists }_{𝑔}{1}_{𝑜}\left(\left({2}_{𝑜}{\in }_{𝑔}{1}_{𝑜}\right){\wedge }_{𝑔}\left({1}_{𝑜}{\in }_{𝑔}\varnothing \right)\right)\right]{\to }_{𝑔}\left({2}_{𝑜}{\in }_{𝑔}{1}_{𝑜}\right)\right)\right]\right]$