Theorem rexrn

Description: Restricted existential quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013) (Revised by Mario Carneiro, 20-Aug-2014)

	Ref	Expression
Hypothesis	rexrn.1	$$⊢x=F\left(y\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	rexrn	$$⊢FFnA\to \left(\exists x\in \mathrm{ran}F\phi \leftrightarrow \exists y\in A\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		rexrn.1	$$⊢x=F\left(y\right)\to \left(\phi \leftrightarrow \psi \right)$$
2		fvexd	$$⊢\left(FFnA\wedge y\in A\right)\to F\left(y\right)\in \mathrm{V}$$
3		fvelrnb	$$⊢FFnA\to \left(x\in \mathrm{ran}F\leftrightarrow \exists y\in AF\left(y\right)=x\right)$$
4		eqcom	$$⊢F\left(y\right)=x\leftrightarrow x=F\left(y\right)$$
5	4	rexbii	$$⊢\exists y\in AF\left(y\right)=x\leftrightarrow \exists y\in Ax=F\left(y\right)$$
6	3 5	bitrdi	$$⊢FFnA\to \left(x\in \mathrm{ran}F\leftrightarrow \exists y\in Ax=F\left(y\right)\right)$$
7	1	adantl	$$⊢\left(FFnA\wedge x=F\left(y\right)\right)\to \left(\phi \leftrightarrow \psi \right)$$
8	2 6 7	rexxfr2d	$$⊢FFnA\to \left(\exists x\in \mathrm{ran}F\phi \leftrightarrow \exists y\in A\psi \right)$$