Definition df-gzext 33415

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 33408	. 2 class AxExt
2		c2o 8291	. . . . . 6 class 2o
3		c0 4256	. . . . . 6 class ∅
4		cgoe 33295	. . . . . 6 class ∈𝑔
5	2, 3, 4	co 7275	. . . . 5 class (2o∈𝑔∅)
6		c1o 8290	. . . . . 6 class 1o
7	2, 6, 4	co 7275	. . . . 5 class (2o∈𝑔1o)
8		cgob 33398	. . . . 5 class ↔𝑔
9	5, 7, 8	co 7275	. . . 4 class ((2o∈𝑔∅) ↔𝑔 (2o∈𝑔1o))
10	9, 2	cgol 33297	. . 3 class ∀𝑔2o((2o∈𝑔∅) ↔𝑔 (2o∈𝑔1o))
11		cgoq 33399	. . . 4 class =𝑔
12	3, 6, 11	co 7275	. . 3 class (∅=𝑔1o)
13		cgoi 33396	. . 3 class →𝑔
14	10, 12, 13	co 7275	. 2 class (∀𝑔2o((2o∈𝑔∅) ↔𝑔 (2o∈𝑔1o)) →𝑔 (∅=𝑔1o))
15	1, 14	wceq 1539	1 wff AxExt = (∀𝑔2o((2o∈𝑔∅) ↔𝑔 (2o∈𝑔1o)) →𝑔 (∅=𝑔1o))

This definition is referenced by: (None)