Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-gzext Structured version   Visualization version   GIF version

Definition df-gzext 32757
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
StepHypRef Expression
1 cgze 32750 . 2 class AxExt
2 c2o 8092 . . . . . 6 class 2o
3 c0 4276 . . . . . 6 class
4 cgoe 32637 . . . . . 6 class 𝑔
52, 3, 4co 7149 . . . . 5 class (2o𝑔∅)
6 c1o 8091 . . . . . 6 class 1o
72, 6, 4co 7149 . . . . 5 class (2o𝑔1o)
8 cgob 32740 . . . . 5 class 𝑔
95, 7, 8co 7149 . . . 4 class ((2o𝑔∅) ↔𝑔 (2o𝑔1o))
109, 2cgol 32639 . . 3 class 𝑔2o((2o𝑔∅) ↔𝑔 (2o𝑔1o))
11 cgoq 32741 . . . 4 class =𝑔
123, 6, 11co 7149 . . 3 class (∅=𝑔1o)
13 cgoi 32738 . . 3 class 𝑔
1410, 12, 13co 7149 . 2 class (∀𝑔2o((2o𝑔∅) ↔𝑔 (2o𝑔1o)) →𝑔 (∅=𝑔1o))
151, 14wceq 1538 1 wff AxExt = (∀𝑔2o((2o𝑔∅) ↔𝑔 (2o𝑔1o)) →𝑔 (∅=𝑔1o))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator