Theorem ssrexf

Description: Restricted existential quantification follows from a subclass relationship. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	ssrexf.1	$$⊢\underset{\_}{Ⅎ}xA$$
	ssrexf.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	ssrexf	$$⊢A\subseteq B\to \left(\exists x\in A\phi \to \exists x\in B\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ssrexf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		ssrexf.2	$$⊢\underset{\_}{Ⅎ}xB$$
3	1 2	nfss	$$⊢ℲxA\subseteq B$$
4		ssel	$$⊢A\subseteq B\to \left(x\in A\to x\in B\right)$$
5	4	anim1d	$$⊢A\subseteq B\to \left(\left(x\in A\wedge \phi \right)\to \left(x\in B\wedge \phi \right)\right)$$
6	3 5	eximd	$$⊢A\subseteq B\to \left(\exists x\left(x\in A\wedge \phi \right)\to \exists x\left(x\in B\wedge \phi \right)\right)$$
7		df-rex	$$⊢\exists x\in A\phi \leftrightarrow \exists x\left(x\in A\wedge \phi \right)$$
8		df-rex	$$⊢\exists x\in B\phi \leftrightarrow \exists x\left(x\in B\wedge \phi \right)$$
9	6 7 8	3imtr4g	$$⊢A\subseteq B\to \left(\exists x\in A\phi \to \exists x\in B\phi \right)$$