Theorem rexima

Description: Existential quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015)

	Ref	Expression
Hypothesis	rexima.x	$$⊢x=F\left(y\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	rexima	$$⊢\left(FFnA\wedge B\subseteq A\right)\to \left(\exists x\in F\left[B\right]\phi \leftrightarrow \exists y\in B\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		rexima.x	$$⊢x=F\left(y\right)\to \left(\phi \leftrightarrow \psi \right)$$
2		fvexd	$$⊢\left(\left(FFnA\wedge B\subseteq A\right)\wedge y\in B\right)\to F\left(y\right)\in \mathrm{V}$$
3		fvelimab	$$⊢\left(FFnA\wedge B\subseteq A\right)\to \left(x\in F\left[B\right]\leftrightarrow \exists y\in BF\left(y\right)=x\right)$$
4		eqcom	$$⊢F\left(y\right)=x\leftrightarrow x=F\left(y\right)$$
5	4	rexbii	$$⊢\exists y\in BF\left(y\right)=x\leftrightarrow \exists y\in Bx=F\left(y\right)$$
6	3 5	bitrdi	$$⊢\left(FFnA\wedge B\subseteq A\right)\to \left(x\in F\left[B\right]\leftrightarrow \exists y\in Bx=F\left(y\right)\right)$$
7	1	adantl	$$⊢\left(\left(FFnA\wedge B\subseteq A\right)\wedge x=F\left(y\right)\right)\to \left(\phi \leftrightarrow \psi \right)$$
8	2 6 7	rexxfr2d	$$⊢\left(FFnA\wedge B\subseteq A\right)\to \left(\exists x\in F\left[B\right]\phi \leftrightarrow \exists y\in B\psi \right)$$