Users' Mathboxes 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 30606
Description: The Godel-set version of the Axiom of Power Sets. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-gzpow AxPow = ∃𝑔1𝑜𝑔2𝑜(∀𝑔1𝑜((1𝑜𝑔2𝑜) ↔𝑔 (1𝑜𝑔∅)) →𝑔 (2𝑜𝑔1𝑜))

Detailed syntax breakdown of Definition df-gzpow
StepHypRef Expression
1 cgzp 30599 . 2 class AxPow
2 c1o 7440 . . . . . . . 8 class 1𝑜
3 c2o 7441 . . . . . . . 8 class 2𝑜
4 cgoe 30569 . . . . . . . 8 class 𝑔
52, 3, 4co 6549 . . . . . . 7 class (1𝑜𝑔2𝑜)
6 c0 3874 . . . . . . . 8 class
72, 6, 4co 6549 . . . . . . 7 class (1𝑜𝑔∅)
8 cgob 30586 . . . . . . 7 class 𝑔
95, 7, 8co 6549 . . . . . 6 class ((1𝑜𝑔2𝑜) ↔𝑔 (1𝑜𝑔∅))
109, 2cgol 30571 . . . . 5 class 𝑔1𝑜((1𝑜𝑔2𝑜) ↔𝑔 (1𝑜𝑔∅))
113, 2, 4co 6549 . . . . 5 class (2𝑜𝑔1𝑜)
12 cgoi 30584 . . . . 5 class 𝑔
1310, 11, 12co 6549 . . . 4 class (∀𝑔1𝑜((1𝑜𝑔2𝑜) ↔𝑔 (1𝑜𝑔∅)) →𝑔 (2𝑜𝑔1𝑜))
1413, 3cgol 30571 . . 3 class 𝑔2𝑜(∀𝑔1𝑜((1𝑜𝑔2𝑜) ↔𝑔 (1𝑜𝑔∅)) →𝑔 (2𝑜𝑔1𝑜))
1514, 2cgox 30588 . 2 class 𝑔1𝑜𝑔2𝑜(∀𝑔1𝑜((1𝑜𝑔2𝑜) ↔𝑔 (1𝑜𝑔∅)) →𝑔 (2𝑜𝑔1𝑜))
161, 15wceq 1475 1 wff AxPow = ∃𝑔1𝑜𝑔2𝑜(∀𝑔1𝑜((1𝑜𝑔2𝑜) ↔𝑔 (1𝑜𝑔∅)) →𝑔 (2𝑜𝑔1𝑜))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator