Theorem rspcedvd

Description: Restricted existential specialization, using implicit substitution. Variant of rspcedv . (Contributed by AV, 27-Nov-2019)

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

Proof

Step	Hyp	Ref	Expression
1		rspcedvd.1	$$⊢\phi \to A\in B$$
2		rspcedvd.2	$$⊢\left(\phi \wedge x=A\right)\to \left(\psi \leftrightarrow \chi \right)$$
3		rspcedvd.3	$$⊢\phi \to \chi$$
4	1 2	rspcedv	$$⊢\phi \to \left(\chi \to \exists x\in B\psi \right)$$
5	3 4	mpd	$$⊢\phi \to \exists x\in B\psi$$