Definition df-gzpow 36189

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

Step	Hyp	Ref	Expression
1		cgzp 36182	. 2 class AxPow
2		c1o 8453	. . . . . . . 8 class 1o
3		c2o 8454	. . . . . . . 8 class 2o
4		cgoe 36067	. . . . . . . 8 class ∈𝑔
5	2, 3, 4	co 7412	. . . . . . 7 class (1o∈𝑔2o)
6		c0 4279	. . . . . . . 8 class ∅
7	2, 6, 4	co 7412	. . . . . . 7 class (1o∈𝑔∅)
8		cgob 36170	. . . . . . 7 class ↔𝑔
9	5, 7, 8	co 7412	. . . . . 6 class ((1o∈𝑔2o) ↔𝑔 (1o∈𝑔∅))
10	9, 2	cgol 36069	. . . . 5 class ∀𝑔1o((1o∈𝑔2o) ↔𝑔 (1o∈𝑔∅))
11	3, 2, 4	co 7412	. . . . 5 class (2o∈𝑔1o)
12		cgoi 36168	. . . . 5 class →𝑔
13	10, 11, 12	co 7412	. . . 4 class (∀𝑔1o((1o∈𝑔2o) ↔𝑔 (1o∈𝑔∅)) →𝑔 (2o∈𝑔1o))
14	13, 3	cgol 36069	. . 3 class ∀𝑔2o(∀𝑔1o((1o∈𝑔2o) ↔𝑔 (1o∈𝑔∅)) →𝑔 (2o∈𝑔1o))
15	14, 2	cgox 36172	. 2 class ∃𝑔1o∀𝑔2o(∀𝑔1o((1o∈𝑔2o) ↔𝑔 (1o∈𝑔∅)) →𝑔 (2o∈𝑔1o))
16	1, 15	wceq 1570	1 wff AxPow = ∃𝑔1o∀𝑔2o(∀𝑔1o((1o∈𝑔2o) ↔𝑔 (1o∈𝑔∅)) →𝑔 (2o∈𝑔1o))

This definition is used by: (None)