Metamath Proof Explorer

Definition df-gzext

Description: The Godel-set version of the Axiom of Extensionality. (Contributed by Mario Carneiro, 14-Jul-2013)

Ref Expression
Assertion df-gzext 
|- AxExt = ( A.g 2o ( ( 2o e.g (/) ) <->g ( 2o e.g 1o ) ) ->g ( (/) =g 1o ) )

Detailed syntax breakdown

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