Definition df-gzext 33315

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 33308	. 2 class AxExt
2		c2o 8261	. . . . . 6 class 2o
3		c0 4253	. . . . . 6 class ∅
4		cgoe 33195	. . . . . 6 class ∈𝑔
5	2, 3, 4	co 7255	. . . . 5 class (2o∈𝑔∅)
6		c1o 8260	. . . . . 6 class 1o
7	2, 6, 4	co 7255	. . . . 5 class (2o∈𝑔1o)
8		cgob 33298	. . . . 5 class ↔𝑔
9	5, 7, 8	co 7255	. . . 4 class ((2o∈𝑔∅) ↔𝑔 (2o∈𝑔1o))
10	9, 2	cgol 33197	. . 3 class ∀𝑔2o((2o∈𝑔∅) ↔𝑔 (2o∈𝑔1o))
11		cgoq 33299	. . . 4 class =𝑔
12	3, 6, 11	co 7255	. . 3 class (∅=𝑔1o)
13		cgoi 33296	. . 3 class →𝑔
14	10, 12, 13	co 7255	. 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)