Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-gzun Structured version   Visualization version   GIF version

Definition df-gzun 32760
 Description: The Godel-set version of the Axiom of Unions. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-gzun AxUn = ∃𝑔1o𝑔2o(∃𝑔1o((2o𝑔1o)∧𝑔(1o𝑔∅)) →𝑔 (2o𝑔1o))

Detailed syntax breakdown of Definition df-gzun
StepHypRef Expression
1 cgzu 32753 . 2 class AxUn
2 c2o 8092 . . . . . . . 8 class 2o
3 c1o 8091 . . . . . . . 8 class 1o
4 cgoe 32637 . . . . . . . 8 class 𝑔
52, 3, 4co 7149 . . . . . . 7 class (2o𝑔1o)
6 c0 4276 . . . . . . . 8 class
73, 6, 4co 7149 . . . . . . 7 class (1o𝑔∅)
8 cgoa 32737 . . . . . . 7 class 𝑔
95, 7, 8co 7149 . . . . . 6 class ((2o𝑔1o)∧𝑔(1o𝑔∅))
109, 3cgox 32742 . . . . 5 class 𝑔1o((2o𝑔1o)∧𝑔(1o𝑔∅))
11 cgoi 32738 . . . . 5 class 𝑔
1210, 5, 11co 7149 . . . 4 class (∃𝑔1o((2o𝑔1o)∧𝑔(1o𝑔∅)) →𝑔 (2o𝑔1o))
1312, 2cgol 32639 . . 3 class 𝑔2o(∃𝑔1o((2o𝑔1o)∧𝑔(1o𝑔∅)) →𝑔 (2o𝑔1o))
1413, 3cgox 32742 . 2 class 𝑔1o𝑔2o(∃𝑔1o((2o𝑔1o)∧𝑔(1o𝑔∅)) →𝑔 (2o𝑔1o))
151, 14wceq 1538 1 wff AxUn = ∃𝑔1o𝑔2o(∃𝑔1o((2o𝑔1o)∧𝑔(1o𝑔∅)) →𝑔 (2o𝑔1o))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator