Definition df-gzext 36305

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

Assertion

Ref	Expression
df-gzext	⊢ AxExt = (∀𝑔2o((2o∈𝑔∅) ↔𝑔 (2o∈𝑔1o)) →𝑔 (∅=𝑔1o))

Detailed syntax breakdown of Definition df-gzext

Step	Hyp	Ref	Expression
1		cgze 36298	. 2 class AxExt
2		c2o 8474	. . . . . 6 class 2o
3		c0 4278	. . . . . 6 class ∅
4		cgoe 36185	. . . . . 6 class ∈𝑔
5	2, 3, 4	co 7421	. . . . 5 class (2o∈𝑔∅)
6		c1o 8473	. . . . . 6 class 1o
7	2, 6, 4	co 7421	. . . . 5 class (2o∈𝑔1o)
8		cgob 36288	. . . . 5 class ↔𝑔
9	5, 7, 8	co 7421	. . . 4 class ((2o∈𝑔∅) ↔𝑔 (2o∈𝑔1o))
10	9, 2	cgol 36187	. . 3 class ∀𝑔2o((2o∈𝑔∅) ↔𝑔 (2o∈𝑔1o))
11		cgoq 36289	. . . 4 class =𝑔
12	3, 6, 11	co 7421	. . 3 class (∅=𝑔1o)
13		cgoi 36286	. . 3 class →𝑔
14	10, 12, 13	co 7421	. 2 class (∀𝑔2o((2o∈𝑔∅) ↔𝑔 (2o∈𝑔1o)) →𝑔 (∅=𝑔1o))
15	1, 14	wceq 1569	1 wff AxExt = (∀𝑔2o((2o∈𝑔∅) ↔𝑔 (2o∈𝑔1o)) →𝑔 (∅=𝑔1o))

This definition is used by: (None)