Definition df-gzpow

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

	Ref	Expression
Assertion	df-gzpow	⊢ AxPow = ∃𝑔 1o ∀𝑔 2o ( ∀𝑔 1o ( ( 1o ∈𝑔 2o ) ↔𝑔 ( 1o ∈𝑔 ∅ ) ) →𝑔 ( 2o ∈𝑔 1o ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgzp	⊢ AxPow
1		c1o	⊢ 1o
2		c2o	⊢ 2o
3		cgoe	⊢ ∈𝑔
4	1 2 3	co	⊢ ( 1o ∈𝑔 2o )
5		cgob	⊢ ↔𝑔
6		c0	⊢ ∅
7	1 6 3	co	⊢ ( 1o ∈𝑔 ∅ )
8	4 7 5	co	⊢ ( ( 1o ∈𝑔 2o ) ↔𝑔 ( 1o ∈𝑔 ∅ ) )
9	8 1	cgol	⊢ ∀𝑔 1o ( ( 1o ∈𝑔 2o ) ↔𝑔 ( 1o ∈𝑔 ∅ ) )
10		cgoi	⊢ →𝑔
11	2 1 3	co	⊢ ( 2o ∈𝑔 1o )
12	9 11 10	co	⊢ ( ∀𝑔 1o ( ( 1o ∈𝑔 2o ) ↔𝑔 ( 1o ∈𝑔 ∅ ) ) →𝑔 ( 2o ∈𝑔 1o ) )
13	12 2	cgol	⊢ ∀𝑔 2o ( ∀𝑔 1o ( ( 1o ∈𝑔 2o ) ↔𝑔 ( 1o ∈𝑔 ∅ ) ) →𝑔 ( 2o ∈𝑔 1o ) )
14	13 1	cgox	⊢ ∃𝑔 1o ∀𝑔 2o ( ∀𝑔 1o ( ( 1o ∈𝑔 2o ) ↔𝑔 ( 1o ∈𝑔 ∅ ) ) →𝑔 ( 2o ∈𝑔 1o ) )
15	0 14	wceq	⊢ AxPow = ∃𝑔 1o ∀𝑔 2o ( ∀𝑔 1o ( ( 1o ∈𝑔 2o ) ↔𝑔 ( 1o ∈𝑔 ∅ ) ) →𝑔 ( 2o ∈𝑔 1o ) )