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 = [\exists_{𝑔} 1_{𝑜} [\forall_{𝑔} 2_{𝑜} ([\forall_{𝑔} 1_{𝑜} ((1_{𝑜} \in_{𝑔} 2_{𝑜}) \leftrightarrow_{𝑔} (1_{𝑜} \in_{𝑔} \emptyset))] \to_{𝑔} (2_{𝑜} \in_{𝑔} 1_{𝑜}))]]$

Step	Hyp	Ref	Expression
0		cgzp	$class AxPow$
1		c1o	$class 1_{𝑜}$
2		c2o	$class 2_{𝑜}$
3		cgoe	$class \in_{𝑔}$
4	1 2 3	co	$class (1_{𝑜} \in_{𝑔} 2_{𝑜})$
5		cgob	$class \leftrightarrow_{𝑔}$
6		c0	$class \emptyset$
7	1 6 3	co	$class (1_{𝑜} \in_{𝑔} \emptyset)$
8	4 7 5	co	$class ((1_{𝑜} \in_{𝑔} 2_{𝑜}) \leftrightarrow_{𝑔} (1_{𝑜} \in_{𝑔} \emptyset))$
9	8 1	cgol	$class [\forall_{𝑔} 1_{𝑜} ((1_{𝑜} \in_{𝑔} 2_{𝑜}) \leftrightarrow_{𝑔} (1_{𝑜} \in_{𝑔} \emptyset))]$
10		cgoi	$class \to_{𝑔}$
11	2 1 3	co	$class (2_{𝑜} \in_{𝑔} 1_{𝑜})$
12	9 11 10	co	$class ([\forall_{𝑔} 1_{𝑜} ((1_{𝑜} \in_{𝑔} 2_{𝑜}) \leftrightarrow_{𝑔} (1_{𝑜} \in_{𝑔} \emptyset))] \to_{𝑔} (2_{𝑜} \in_{𝑔} 1_{𝑜}))$
13	12 2	cgol	$class [\forall_{𝑔} 2_{𝑜} ([\forall_{𝑔} 1_{𝑜} ((1_{𝑜} \in_{𝑔} 2_{𝑜}) \leftrightarrow_{𝑔} (1_{𝑜} \in_{𝑔} \emptyset))] \to_{𝑔} (2_{𝑜} \in_{𝑔} 1_{𝑜}))]$
14	13 1	cgox	$class [\exists_{𝑔} 1_{𝑜} [\forall_{𝑔} 2_{𝑜} ([\forall_{𝑔} 1_{𝑜} ((1_{𝑜} \in_{𝑔} 2_{𝑜}) \leftrightarrow_{𝑔} (1_{𝑜} \in_{𝑔} \emptyset))] \to_{𝑔} (2_{𝑜} \in_{𝑔} 1_{𝑜}))]]$
15	0 14	wceq	$wff AxPow = [\exists_{𝑔} 1_{𝑜} [\forall_{𝑔} 2_{𝑜} ([\forall_{𝑔} 1_{𝑜} ((1_{𝑜} \in_{𝑔} 2_{𝑜}) \leftrightarrow_{𝑔} (1_{𝑜} \in_{𝑔} \emptyset))] \to_{𝑔} (2_{𝑜} \in_{𝑔} 1_{𝑜}))]]$

Metamath Proof Explorer