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

Definition df-gzpow 32759
 Description: The Godel-set version of the Axiom of Power Sets. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-gzpow AxPow = ∃𝑔1o𝑔2o(∀𝑔1o((1o𝑔2o) ↔𝑔 (1o𝑔∅)) →𝑔 (2o𝑔1o))

Detailed syntax breakdown of Definition df-gzpow
StepHypRef Expression
1 cgzp 32752 . 2 class AxPow
2 c1o 8091 . . . . . . . 8 class 1o
3 c2o 8092 . . . . . . . 8 class 2o
4 cgoe 32637 . . . . . . . 8 class 𝑔
52, 3, 4co 7149 . . . . . . 7 class (1o𝑔2o)
6 c0 4276 . . . . . . . 8 class
72, 6, 4co 7149 . . . . . . 7 class (1o𝑔∅)
8 cgob 32740 . . . . . . 7 class 𝑔
95, 7, 8co 7149 . . . . . 6 class ((1o𝑔2o) ↔𝑔 (1o𝑔∅))
109, 2cgol 32639 . . . . 5 class 𝑔1o((1o𝑔2o) ↔𝑔 (1o𝑔∅))
113, 2, 4co 7149 . . . . 5 class (2o𝑔1o)
12 cgoi 32738 . . . . 5 class 𝑔
1310, 11, 12co 7149 . . . 4 class (∀𝑔1o((1o𝑔2o) ↔𝑔 (1o𝑔∅)) →𝑔 (2o𝑔1o))
1413, 3cgol 32639 . . 3 class 𝑔2o(∀𝑔1o((1o𝑔2o) ↔𝑔 (1o𝑔∅)) →𝑔 (2o𝑔1o))
1514, 2cgox 32742 . 2 class 𝑔1o𝑔2o(∀𝑔1o((1o𝑔2o) ↔𝑔 (1o𝑔∅)) →𝑔 (2o𝑔1o))
161, 15wceq 1538 1 wff AxPow = ∃𝑔1o𝑔2o(∀𝑔1o((1o𝑔2o) ↔𝑔 (1o𝑔∅)) →𝑔 (2o𝑔1o))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator