Metamath Proof Explorer

Definition df-gzun

Description: The Godel-set version of the Axiom of Unions. (Contributed by Mario Carneiro, 14-Jul-2013)

Ref Expression
Assertion 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

Step Hyp Ref Expression
0 cgzu 
 |-  AxUn
1 c1o 
 |-  1o
2 c2o 
 |-  2o
3 cgoe 
 |-  e.g
4 2 1 3 co 
 |-  ( 2o e.g 1o )
5 cgoa 
 |-  /\g
6 c0 
 |-  (/)
7 1 6 3 co 
 |-  ( 1o e.g (/) )
8 4 7 5 co 
 |-  ( ( 2o e.g 1o ) /\g ( 1o e.g (/) ) )
9 8 1 cgox 
 |-  E.g 1o ( ( 2o e.g 1o ) /\g ( 1o e.g (/) ) )
10 cgoi 
 |-  ->g
11 9 4 10 co 
 |-  ( E.g 1o ( ( 2o e.g 1o ) /\g ( 1o e.g (/) ) ) ->g ( 2o e.g 1o ) )
12 11 2 cgol 
 |-  A.g 2o ( E.g 1o ( ( 2o e.g 1o ) /\g ( 1o e.g (/) ) ) ->g ( 2o e.g 1o ) )
13 12 1 cgox 
 |-  E.g 1o A.g 2o ( E.g 1o ( ( 2o e.g 1o ) /\g ( 1o e.g (/) ) ) ->g ( 2o e.g 1o ) )
14 0 13 wceq 
 |-  AxUn = E.g 1o A.g 2o ( E.g 1o ( ( 2o e.g 1o ) /\g ( 1o e.g (/) ) ) ->g ( 2o e.g 1o ) )