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

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

Detailed syntax breakdown of Definition df-gzun
StepHypRef Expression
1 cgzu 24351 . 2  class  AxUn
2 c2o 6560 . . . . . . . 8  class  2o
3 c1o 6559 . . . . . . . 8  class  1o
4 cgoe 24320 . . . . . . . 8  class  e.g
52, 3, 4co 5945 . . . . . . 7  class  ( 2o 
e.g  1o )
6 c0 3531 . . . . . . . 8  class  (/)
73, 6, 4co 5945 . . . . . . 7  class  ( 1o 
e.g  (/) )
8 cgoa 24334 . . . . . . 7  class  /\g
95, 7, 8co 5945 . . . . . 6  class  ( ( 2o  e.g  1o ) 
/\g  ( 1o  e.g  (/) ) )
109, 3cgox 24339 . . . . 5  class  E.g 1o ( ( 2o  e.g  1o )  /\g  ( 1o  e.g  (/) ) )
11 cgoi 24335 . . . . 5  class  ->g
1210, 5, 11co 5945 . . . 4  class  ( E.g 1o ( ( 2o  e.g  1o )  /\g  ( 1o  e.g  (/) ) )  ->g  ( 2o  e.g  1o ) )
1312, 2cgol 24322 . . 3  class  A.g 2o ( E.g 1o ( ( 2o  e.g  1o ) 
/\g  ( 1o  e.g  (/) ) )  ->g  ( 2o 
e.g  1o ) )
1413, 3cgox 24339 . 2  class  E.g 1o A.g
2o ( E.g 1o ( ( 2o  e.g  1o )  /\g  ( 1o  e.g  (/) ) )  ->g  ( 2o  e.g  1o ) )
151, 14wceq 1642 1  wff  AxUn  =  E.g
1o A.g 2o ( E.g 1o ( ( 2o  e.g  1o )  /\g  ( 1o  e.g  (/) ) )  ->g  ( 2o  e.g  1o ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator