Theorem abrexex2g

Description: Existence of an existentially restricted class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	abrexex2g	$$⊢\left(A\in V\wedge \forall x\in A\left\{y|\phi \right\}\in W\right)\to \left\{y|\exists x\in A\phi \right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		nfv	$$⊢Ⅎz\exists x\in A\phi$$
2		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
3		nfs1v	$$⊢Ⅎy\left[z/y\right]\phi$$
4	2 3	nfrex	$$⊢Ⅎy\exists x\in A\left[z/y\right]\phi$$
5		sbequ12	$$⊢y=z\to \left(\phi \leftrightarrow \left[z/y\right]\phi \right)$$
6	5	rexbidv	$$⊢y=z\to \left(\exists x\in A\phi \leftrightarrow \exists x\in A\left[z/y\right]\phi \right)$$
7	1 4 6	cbvabw	$$⊢\left\{y|\exists x\in A\phi \right\}=\left\{z|\exists x\in A\left[z/y\right]\phi \right\}$$
8		df-clab	$$⊢z\in \left\{y|\phi \right\}\leftrightarrow \left[z/y\right]\phi$$
9	8	rexbii	$$⊢\exists x\in Az\in \left\{y|\phi \right\}\leftrightarrow \exists x\in A\left[z/y\right]\phi$$
10	9	abbii	$$⊢\left\{z|\exists x\in Az\in \left\{y|\phi \right\}\right\}=\left\{z|\exists x\in A\left[z/y\right]\phi \right\}$$
11	7 10	eqtr4i	$$⊢\left\{y|\exists x\in A\phi \right\}=\left\{z|\exists x\in Az\in \left\{y|\phi \right\}\right\}$$
12		df-iun	$$⊢\bigcup _{x\in A}\left\{y|\phi \right\}=\left\{z|\exists x\in Az\in \left\{y|\phi \right\}\right\}$$
13		iunexg	$$⊢\left(A\in V\wedge \forall x\in A\left\{y|\phi \right\}\in W\right)\to \bigcup _{x\in A}\left\{y|\phi \right\}\in \mathrm{V}$$
14	12 13	eqeltrrid	$$⊢\left(A\in V\wedge \forall x\in A\left\{y|\phi \right\}\in W\right)\to \left\{z|\exists x\in Az\in \left\{y|\phi \right\}\right\}\in \mathrm{V}$$
15	11 14	eqeltrid	$$⊢\left(A\in V\wedge \forall x\in A\left\{y|\phi \right\}\in W\right)\to \left\{y|\exists x\in A\phi \right\}\in \mathrm{V}$$