Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-gzpow Unicode version

Definition df-gzpow 23953
Description: The Godel-set version of the Axiom of Power Sets. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
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 of Definition df-gzpow
StepHypRef Expression
1 cgzp 23946 . 2  class  AxPow
2 c1o 6472 . . . . . . . 8  class  1o
3 c2o 6473 . . . . . . . 8  class  2o
4 cgoe 23916 . . . . . . . 8  class  e.g
52, 3, 4co 5858 . . . . . . 7  class  ( 1o 
e.g  2o )
6 c0 3455 . . . . . . . 8  class  (/)
72, 6, 4co 5858 . . . . . . 7  class  ( 1o 
e.g  (/) )
8 cgob 23933 . . . . . . 7  class  <->g
95, 7, 8co 5858 . . . . . 6  class  ( ( 1o  e.g  2o ) 
<->g  ( 1o  e.g  (/) ) )
109, 2cgol 23918 . . . . 5  class  A.g 1o ( ( 1o  e.g  2o )  <->g  ( 1o  e.g  (/) ) )
113, 2, 4co 5858 . . . . 5  class  ( 2o 
e.g  1o )
12 cgoi 23931 . . . . 5  class  ->g
1310, 11, 12co 5858 . . . 4  class  ( A.g 1o ( ( 1o  e.g  2o )  <->g  ( 1o  e.g  (/) ) )  ->g  ( 2o 
e.g  1o ) )
1413, 3cgol 23918 . . 3  class  A.g 2o ( A.g 1o ( ( 1o  e.g  2o ) 
<->g  ( 1o  e.g  (/) ) ) 
->g  ( 2o  e.g  1o ) )
1514, 2cgox 23935 . 2  class  E.g 1o A.g
2o ( A.g 1o ( ( 1o  e.g  2o )  <->g  ( 1o  e.g  (/) ) )  ->g  ( 2o 
e.g  1o ) )
161, 15wceq 1623 1  wff  AxPow  =  E.g 1o A.g 2o ( A.g 1o ( ( 1o  e.g  2o )  <->g  ( 1o  e.g  (/) ) )  ->g  ( 2o 
e.g  1o ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator