Theorem reximssdv

Description: Derivation of a restricted existential quantification over a subset (the second hypothesis implies A C_ B ), deduction form. (Contributed by AV, 21-Aug-2022)

	Ref	Expression
Hypotheses	reximssdv.1	$$⊢\phi \to \exists x\in B\psi$$
	reximssdv.2	$$⊢\left(\phi \wedge \left(x\in B\wedge \psi \right)\right)\to x\in A$$
	reximssdv.3	$$⊢\left(\phi \wedge \left(x\in B\wedge \psi \right)\right)\to \chi$$
Assertion	reximssdv	$$⊢\phi \to \exists x\in A\chi$$

Proof

Step	Hyp	Ref	Expression
1		reximssdv.1	$$⊢\phi \to \exists x\in B\psi$$
2		reximssdv.2	$$⊢\left(\phi \wedge \left(x\in B\wedge \psi \right)\right)\to x\in A$$
3		reximssdv.3	$$⊢\left(\phi \wedge \left(x\in B\wedge \psi \right)\right)\to \chi$$
4	2 3	jca	$$⊢\left(\phi \wedge \left(x\in B\wedge \psi \right)\right)\to \left(x\in A\wedge \chi \right)$$
5	4	ex	$$⊢\phi \to \left(\left(x\in B\wedge \psi \right)\to \left(x\in A\wedge \chi \right)\right)$$
6	5	reximdv2	$$⊢\phi \to \left(\exists x\in B\psi \to \exists x\in A\chi \right)$$
7	1 6	mpd	$$⊢\phi \to \exists x\in A\chi$$