# Metamath Proof Explorer

## Definition df-gzreg

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

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

### Detailed syntax breakdown

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