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

Definition df-gzext 23951
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 23944 . 2  class  AxExt
2 c2o 6473 . . . . . 6  class  2o
3 c0 3455 . . . . . 6  class  (/)
4 cgoe 23916 . . . . . 6  class  e.g
52, 3, 4co 5858 . . . . 5  class  ( 2o 
e.g  (/) )
6 c1o 6472 . . . . . 6  class  1o
72, 6, 4co 5858 . . . . 5  class  ( 2o 
e.g  1o )
8 cgob 23933 . . . . 5  class  <->g
95, 7, 8co 5858 . . . 4  class  ( ( 2o  e.g  (/) )  <->g  ( 2o  e.g  1o ) )
109, 2cgol 23918 . . 3  class  A.g 2o ( ( 2o  e.g  (/) )  <->g  ( 2o  e.g  1o ) )
11 cgoq 23934 . . . 4  class  =g
123, 6, 11co 5858 . . 3  class  ( (/)  =g  1o )
13 cgoi 23931 . . 3  class  ->g
1410, 12, 13co 5858 . 2  class  ( A.g 2o ( ( 2o  e.g  (/) )  <->g  ( 2o  e.g  1o ) )  ->g  ( (/)  =g  1o ) )
151, 14wceq 1623 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