Definition df-gzpow 35460

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 35453	. 2 class AxPow
2		c1o 8499	. . . . . . . 8 class 1o
3		c2o 8500	. . . . . . . 8 class 2o
4		cgoe 35338	. . . . . . . 8 class ∈𝑔
5	2, 3, 4	co 7431	. . . . . . 7 class (1o∈𝑔2o)
6		c0 4333	. . . . . . . 8 class ∅
7	2, 6, 4	co 7431	. . . . . . 7 class (1o∈𝑔∅)
8		cgob 35441	. . . . . . 7 class ↔𝑔
9	5, 7, 8	co 7431	. . . . . 6 class ((1o∈𝑔2o) ↔𝑔 (1o∈𝑔∅))
10	9, 2	cgol 35340	. . . . 5 class ∀𝑔1o((1o∈𝑔2o) ↔𝑔 (1o∈𝑔∅))
11	3, 2, 4	co 7431	. . . . 5 class (2o∈𝑔1o)
12		cgoi 35439	. . . . 5 class →𝑔
13	10, 11, 12	co 7431	. . . 4 class (∀𝑔1o((1o∈𝑔2o) ↔𝑔 (1o∈𝑔∅)) →𝑔 (2o∈𝑔1o))
14	13, 3	cgol 35340	. . 3 class ∀𝑔2o(∀𝑔1o((1o∈𝑔2o) ↔𝑔 (1o∈𝑔∅)) →𝑔 (2o∈𝑔1o))
15	14, 2	cgox 35443	. 2 class ∃𝑔1o∀𝑔2o(∀𝑔1o((1o∈𝑔2o) ↔𝑔 (1o∈𝑔∅)) →𝑔 (2o∈𝑔1o))
16	1, 15	wceq 1540	1 wff AxPow = ∃𝑔1o∀𝑔2o(∀𝑔1o((1o∈𝑔2o) ↔𝑔 (1o∈𝑔∅)) →𝑔 (2o∈𝑔1o))

This definition is referenced by: (None)