df-gzun

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

		Ref	Expression
	Assertion	df-gzun	$⊢ AxUn = [\exists_{𝑔} 1_{𝑜} [\forall_{𝑔} 2_{𝑜} ([\exists_{𝑔} 1_{𝑜} ((2_{𝑜} \in_{𝑔} 1_{𝑜}) \land_{𝑔} (1_{𝑜} \in_{𝑔} \emptyset))] \to_{𝑔} (2_{𝑜} \in_{𝑔} 1_{𝑜}))]]$

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

Metamath Proof Explorer