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 32597
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 32590 . 2 class AxExt
2 c2o 8085 . . . . . 6 class 2o
3 c0 4288 . . . . . 6 class
4 cgoe 32477 . . . . . 6 class 𝑔
52, 3, 4co 7145 . . . . 5 class (2o𝑔∅)
6 c1o 8084 . . . . . 6 class 1o
72, 6, 4co 7145 . . . . 5 class (2o𝑔1o)
8 cgob 32580 . . . . 5 class 𝑔
95, 7, 8co 7145 . . . 4 class ((2o𝑔∅) ↔𝑔 (2o𝑔1o))
109, 2cgol 32479 . . 3 class 𝑔2o((2o𝑔∅) ↔𝑔 (2o𝑔1o))
11 cgoq 32581 . . . 4 class =𝑔
123, 6, 11co 7145 . . 3 class (∅=𝑔1o)
13 cgoi 32578 . . 3 class 𝑔
1410, 12, 13co 7145 . 2 class (∀𝑔2o((2o𝑔∅) ↔𝑔 (2o𝑔1o)) →𝑔 (∅=𝑔1o))
151, 14wceq 1528 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