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 = E.g 1o A.g 2o ( A.g 1o ( ( 1o e.g 2o ) <->g ( 1o e.g (/) ) ) ->g ( 2o e.g 1o ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgzp 
 |-  AxPow
1 c1o 
 |-  1o
2 c2o 
 |-  2o
3 cgoe 
 |-  e.g
4 1 2 3 co 
 |-  ( 1o e.g 2o )
5 cgob 
 |-  <->g
6 c0 
 |-  (/)
7 1 6 3 co 
 |-  ( 1o e.g (/) )
8 4 7 5 co 
 |-  ( ( 1o e.g 2o ) <->g ( 1o e.g (/) ) )
9 8 1 cgol 
 |-  A.g 1o ( ( 1o e.g 2o ) <->g ( 1o e.g (/) ) )
10 cgoi 
 |-  ->g
11 2 1 3 co 
 |-  ( 2o e.g 1o )
12 9 11 10 co 
 |-  ( A.g 1o ( ( 1o e.g 2o ) <->g ( 1o e.g (/) ) ) ->g ( 2o e.g 1o ) )
13 12 2 cgol 
 |-  A.g 2o ( A.g 1o ( ( 1o e.g 2o ) <->g ( 1o e.g (/) ) ) ->g ( 2o e.g 1o ) )
14 13 1 cgox 
 |-  E.g 1o A.g 2o ( A.g 1o ( ( 1o e.g 2o ) <->g ( 1o e.g (/) ) ) ->g ( 2o e.g 1o ) )
15 0 14 wceq 
 |-  AxPow = E.g 1o A.g 2o ( A.g 1o ( ( 1o e.g 2o ) <->g ( 1o e.g (/) ) ) ->g ( 2o e.g 1o ) )