Definition df-gzext 31350

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

Step	Hyp	Ref	Expression
1		cgze 31343	. 2 class AxExt
2		c2o 7554	. . . . . 6 class 2o
3		c0 3915	. . . . . 6 class (/)
4		cgoe 31315	. . . . . 6 class e.g
5	2, 3, 4	co 6650	. . . . 5 class ( 2o e.g (/) )
6		c1o 7553	. . . . . 6 class 1o
7	2, 6, 4	co 6650	. . . . 5 class ( 2o e.g 1o )
8		cgob 31332	. . . . 5 class <->g
9	5, 7, 8	co 6650	. . . 4 class ( ( 2o e.g (/) ) <->g ( 2o e.g 1o ) )
10	9, 2	cgol 31317	. . 3 class A.g 2o ( ( 2o e.g (/) ) <->g ( 2o e.g 1o ) )
11		cgoq 31333	. . . 4 class =g
12	3, 6, 11	co 6650	. . 3 class ( (/) =g 1o )
13		cgoi 31330	. . 3 class ->g
14	10, 12, 13	co 6650	. 2 class ( A.g 2o ( ( 2o e.g (/) ) <->g ( 2o e.g 1o ) ) ->g ( (/) =g 1o ) )
15	1, 14	wceq 1483	1 wff AxExt = ( A.g 2o ( ( 2o e.g (/) ) <->g ( 2o e.g 1o ) ) ->g ( (/) =g 1o ) )

This definition is referenced by: (None)