Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-gzreg Unicode version

Definition df-gzreg 23970
Description: The Godel-set version of the Axiom of Regularity. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-gzreg  |-  AxReg  =  (
E.g 1o ( 1o  e.g  (/) )  ->g  E.g 1o ( ( 1o  e.g  (/) )  /\g  A.g
2o ( ( 2o 
e.g  1o )  ->g  -.g ( 2o  e.g  (/) ) ) ) )

Detailed syntax breakdown of Definition df-gzreg
StepHypRef Expression
1 cgzg 23963 . 2  class  AxReg
2 c1o 6488 . . . . 5  class  1o
3 c0 3468 . . . . 5  class  (/)
4 cgoe 23931 . . . . 5  class  e.g
52, 3, 4co 5874 . . . 4  class  ( 1o 
e.g  (/) )
65, 2cgox 23950 . . 3  class  E.g 1o ( 1o  e.g  (/) )
7 c2o 6489 . . . . . . . 8  class  2o
87, 2, 4co 5874 . . . . . . 7  class  ( 2o 
e.g  1o )
97, 3, 4co 5874 . . . . . . . 8  class  ( 2o 
e.g  (/) )
109cgon 23944 . . . . . . 7  class  -.g ( 2o  e.g  (/) )
11 cgoi 23946 . . . . . . 7  class  ->g
128, 10, 11co 5874 . . . . . 6  class  ( ( 2o  e.g  1o ) 
->g  -.g ( 2o  e.g  (/) ) )
1312, 7cgol 23933 . . . . 5  class  A.g 2o ( ( 2o  e.g  1o )  ->g  -.g ( 2o 
e.g  (/) ) )
14 cgoa 23945 . . . . 5  class  /\g
155, 13, 14co 5874 . . . 4  class  ( ( 1o  e.g  (/) )  /\g  A.g
2o ( ( 2o 
e.g  1o )  ->g  -.g ( 2o  e.g  (/) ) ) )
1615, 2cgox 23950 . . 3  class  E.g 1o ( ( 1o  e.g  (/) )  /\g  A.g 2o ( ( 2o  e.g  1o )  ->g  -.g ( 2o  e.g  (/) ) ) )
176, 16, 11co 5874 . 2  class  ( E.g 1o ( 1o  e.g  (/) )  ->g  E.g
1o ( ( 1o 
e.g  (/) )  /\g  A.g 2o ( ( 2o  e.g  1o )  ->g  -.g ( 2o 
e.g  (/) ) ) ) )
181, 17wceq 1632 1  wff  AxReg  =  (
E.g 1o ( 1o  e.g  (/) )  ->g  E.g 1o ( ( 1o  e.g  (/) )  /\g  A.g
2o ( ( 2o 
e.g  1o )  ->g  -.g ( 2o  e.g  (/) ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator