Definition df-gzpow 31352

Description: The Godel-set version of the Axiom of Power Sets. (Contributed by Mario Carneiro, 14-Jul-2013.)

Assertion

Ref	Expression
df-gzpow	|- AxPow = E.g 1o A.g 2o ( A.g 1o ( ( 1o e.g 2o ) <->g ( 1o e.g (/) ) ) ->g ( 2o e.g 1o ) )

Detailed syntax breakdown of Definition df-gzpow

Step	Hyp	Ref	Expression
1		cgzp 31345	. 2 class AxPow
2		c1o 7553	. . . . . . . 8 class 1o
3		c2o 7554	. . . . . . . 8 class 2o
4		cgoe 31315	. . . . . . . 8 class e.g
5	2, 3, 4	co 6650	. . . . . . 7 class ( 1o e.g 2o )
6		c0 3915	. . . . . . . 8 class (/)
7	2, 6, 4	co 6650	. . . . . . 7 class ( 1o e.g (/) )
8		cgob 31332	. . . . . . 7 class <->g
9	5, 7, 8	co 6650	. . . . . 6 class ( ( 1o e.g 2o ) <->g ( 1o e.g (/) ) )
10	9, 2	cgol 31317	. . . . 5 class A.g 1o ( ( 1o e.g 2o ) <->g ( 1o e.g (/) ) )
11	3, 2, 4	co 6650	. . . . 5 class ( 2o e.g 1o )
12		cgoi 31330	. . . . 5 class ->g
13	10, 11, 12	co 6650	. . . 4 class ( A.g 1o ( ( 1o e.g 2o ) <->g ( 1o e.g (/) ) ) ->g ( 2o e.g 1o ) )
14	13, 3	cgol 31317	. . 3 class A.g 2o ( A.g 1o ( ( 1o e.g 2o ) <->g ( 1o e.g (/) ) ) ->g ( 2o e.g 1o ) )
15	14, 2	cgox 31334	. 2 class E.g 1o A.g 2o ( A.g 1o ( ( 1o e.g 2o ) <->g ( 1o e.g (/) ) ) ->g ( 2o e.g 1o ) )
16	1, 15	wceq 1483	1 wff AxPow = E.g 1o A.g 2o ( A.g 1o ( ( 1o e.g 2o ) <->g ( 1o e.g (/) ) ) ->g ( 2o e.g 1o ) )

This definition is referenced by: (None)