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

Definition df-gzun 23954
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 23947 . 2  class  AxUn
2 c2o 6473 . . . . . . . 8  class  2o
3 c1o 6472 . . . . . . . 8  class  1o
4 cgoe 23916 . . . . . . . 8  class  e.g
52, 3, 4co 5858 . . . . . . 7  class  ( 2o 
e.g  1o )
6 c0 3455 . . . . . . . 8  class  (/)
73, 6, 4co 5858 . . . . . . 7  class  ( 1o 
e.g  (/) )
8 cgoa 23930 . . . . . . 7  class  /\g
95, 7, 8co 5858 . . . . . 6  class  ( ( 2o  e.g  1o ) 
/\g  ( 1o  e.g  (/) ) )
109, 3cgox 23935 . . . . 5  class  E.g 1o ( ( 2o  e.g  1o )  /\g  ( 1o  e.g  (/) ) )
11 cgoi 23931 . . . . 5  class  ->g
1210, 5, 11co 5858 . . . 4  class  ( E.g 1o ( ( 2o  e.g  1o )  /\g  ( 1o  e.g  (/) ) )  ->g  ( 2o  e.g  1o ) )
1312, 2cgol 23918 . . 3  class  A.g 2o ( E.g 1o ( ( 2o  e.g  1o ) 
/\g  ( 1o  e.g  (/) ) )  ->g  ( 2o 
e.g  1o ) )
1413, 3cgox 23935 . 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 1623 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