# Metamath Proof Explorer

## Definition df-gzpow

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

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

### Detailed syntax breakdown

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