Theorem abexex

Description: A condition where a class abstraction continues to exist after its wff is existentially quantified. (Contributed by NM, 4-Mar-2007)

	Ref	Expression
Hypotheses	abexex.1	$$⊢A\in \mathrm{V}$$
	abexex.2	$$⊢\phi \to x\in A$$
	abexex.3	$$⊢\left\{y|\phi \right\}\in \mathrm{V}$$
Assertion	abexex	$$⊢\left\{y|\exists x\phi \right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		abexex.1	$$⊢A\in \mathrm{V}$$
2		abexex.2	$$⊢\phi \to x\in A$$
3		abexex.3	$$⊢\left\{y|\phi \right\}\in \mathrm{V}$$
4		df-rex	$$⊢\exists x\in A\phi \leftrightarrow \exists x\left(x\in A\wedge \phi \right)$$
5	2	pm4.71ri	$$⊢\phi \leftrightarrow \left(x\in A\wedge \phi \right)$$
6	5	exbii	$$⊢\exists x\phi \leftrightarrow \exists x\left(x\in A\wedge \phi \right)$$
7	4 6	bitr4i	$$⊢\exists x\in A\phi \leftrightarrow \exists x\phi$$
8	7	abbii	$$⊢\left\{y|\exists x\in A\phi \right\}=\left\{y|\exists x\phi \right\}$$
9	1 3	abrexex2	$$⊢\left\{y|\exists x\in A\phi \right\}\in \mathrm{V}$$
10	8 9	eqeltrri	$$⊢\left\{y|\exists x\phi \right\}\in \mathrm{V}$$