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 AxPow = 𝑔 1 𝑜 𝑔 2 𝑜 𝑔 1 𝑜 1 𝑜 𝑔 2 𝑜 𝑔 1 𝑜 𝑔 𝑔 2 𝑜 𝑔 1 𝑜

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgzp class AxPow
1 c1o class 1 𝑜
2 c2o class 2 𝑜
3 cgoe class 𝑔
4 1 2 3 co class 1 𝑜 𝑔 2 𝑜
5 cgob class 𝑔
6 c0 class
7 1 6 3 co class 1 𝑜 𝑔
8 4 7 5 co class 1 𝑜 𝑔 2 𝑜 𝑔 1 𝑜 𝑔
9 8 1 cgol class 𝑔 1 𝑜 1 𝑜 𝑔 2 𝑜 𝑔 1 𝑜 𝑔
10 cgoi class 𝑔
11 2 1 3 co class 2 𝑜 𝑔 1 𝑜
12 9 11 10 co class 𝑔 1 𝑜 1 𝑜 𝑔 2 𝑜 𝑔 1 𝑜 𝑔 𝑔 2 𝑜 𝑔 1 𝑜
13 12 2 cgol class 𝑔 2 𝑜 𝑔 1 𝑜 1 𝑜 𝑔 2 𝑜 𝑔 1 𝑜 𝑔 𝑔 2 𝑜 𝑔 1 𝑜
14 13 1 cgox class 𝑔 1 𝑜 𝑔 2 𝑜 𝑔 1 𝑜 1 𝑜 𝑔 2 𝑜 𝑔 1 𝑜 𝑔 𝑔 2 𝑜 𝑔 1 𝑜
15 0 14 wceq wff AxPow = 𝑔 1 𝑜 𝑔 2 𝑜 𝑔 1 𝑜 1 𝑜 𝑔 2 𝑜 𝑔 1 𝑜 𝑔 𝑔 2 𝑜 𝑔 1 𝑜