Theorem abrexexd

Description: Existence of a class abstraction of existentially restricted sets. (Contributed by Thierry Arnoux, 10-May-2017)

	Ref	Expression
Hypotheses	abrexexd.0	$$⊢\underset{\_}{Ⅎ}xA$$
	abrexexd.1	$$⊢\phi \to A\in \mathrm{V}$$
Assertion	abrexexd	$$⊢\phi \to \left\{y|\exists x\in Ay=B\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		abrexexd.0	$$⊢\underset{\_}{Ⅎ}xA$$
2		abrexexd.1	$$⊢\phi \to A\in \mathrm{V}$$
3		rnopab	$$⊢\mathrm{ran}\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}=\left\{y|\exists x\left(x\in A\wedge y=B\right)\right\}$$
4		df-mpt	$$⊢\left(x\in A⟼B\right)=\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
5	4	rneqi	$$⊢\mathrm{ran}\left(x\in A⟼B\right)=\mathrm{ran}\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
6		df-rex	$$⊢\exists x\in Ay=B\leftrightarrow \exists x\left(x\in A\wedge y=B\right)$$
7	6	abbii	$$⊢\left\{y|\exists x\in Ay=B\right\}=\left\{y|\exists x\left(x\in A\wedge y=B\right)\right\}$$
8	3 5 7	3eqtr4i	$$⊢\mathrm{ran}\left(x\in A⟼B\right)=\left\{y|\exists x\in Ay=B\right\}$$
9		funmpt	$$⊢\mathrm{Fun}\left(x\in A⟼B\right)$$
10		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
11	10	dmmpt	$$⊢\mathrm{dom}\left(x\in A⟼B\right)=\left\{x\in A|B\in \mathrm{V}\right\}$$
12	1	rabexgfGS	$$⊢A\in \mathrm{V}\to \left\{x\in A|B\in \mathrm{V}\right\}\in \mathrm{V}$$
13	11 12	eqeltrid	$$⊢A\in \mathrm{V}\to \mathrm{dom}\left(x\in A⟼B\right)\in \mathrm{V}$$
14		funex	$$⊢\left(\mathrm{Fun}\left(x\in A⟼B\right)\wedge \mathrm{dom}\left(x\in A⟼B\right)\in \mathrm{V}\right)\to \left(x\in A⟼B\right)\in \mathrm{V}$$
15	9 13 14	sylancr	$$⊢A\in \mathrm{V}\to \left(x\in A⟼B\right)\in \mathrm{V}$$
16		rnexg	$$⊢\left(x\in A⟼B\right)\in \mathrm{V}\to \mathrm{ran}\left(x\in A⟼B\right)\in \mathrm{V}$$
17	2 15 16	3syl	$$⊢\phi \to \mathrm{ran}\left(x\in A⟼B\right)\in \mathrm{V}$$
18	8 17	eqeltrrid	$$⊢\phi \to \left\{y|\exists x\in Ay=B\right\}\in \mathrm{V}$$