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

Definition df-gzext 25055
Description: The Godel-set version of the Axiom of Extensionality. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-gzext  |-  AxExt  =  (
A.g 2o ( ( 2o 
e.g  (/) )  <->g  ( 2o 
e.g  1o ) )  ->g  ( (/)  =g  1o ) )

Detailed syntax breakdown of Definition df-gzext
StepHypRef Expression
1 cgze 25048 . 2  class  AxExt
2 c2o 6718 . . . . . 6  class  2o
3 c0 3628 . . . . . 6  class  (/)
4 cgoe 25020 . . . . . 6  class  e.g
52, 3, 4co 6081 . . . . 5  class  ( 2o 
e.g  (/) )
6 c1o 6717 . . . . . 6  class  1o
72, 6, 4co 6081 . . . . 5  class  ( 2o 
e.g  1o )
8 cgob 25037 . . . . 5  class  <->g
95, 7, 8co 6081 . . . 4  class  ( ( 2o  e.g  (/) )  <->g  ( 2o  e.g  1o ) )
109, 2cgol 25022 . . 3  class  A.g 2o ( ( 2o  e.g  (/) )  <->g  ( 2o  e.g  1o ) )
11 cgoq 25038 . . . 4  class  =g
123, 6, 11co 6081 . . 3  class  ( (/)  =g  1o )
13 cgoi 25035 . . 3  class  ->g
1410, 12, 13co 6081 . 2  class  ( A.g 2o ( ( 2o  e.g  (/) )  <->g  ( 2o  e.g  1o ) )  ->g  ( (/)  =g  1o ) )
151, 14wceq 1652 1  wff  AxExt  =  (
A.g 2o ( ( 2o 
e.g  (/) )  <->g  ( 2o 
e.g  1o ) )  ->g  ( (/)  =g  1o ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator