df-gzext

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

		Ref	Expression
	Assertion	df-gzext	$⊢ AxExt = [\forall_{𝑔} 2_{𝑜} ((2_{𝑜} \in_{𝑔} \emptyset) \leftrightarrow_{𝑔} (2_{𝑜} \in_{𝑔} 1_{𝑜}))] \to_{𝑔} (\emptyset =_{𝑔} 1_{𝑜})$

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

Metamath Proof Explorer