Theorem rspceb2dv

Description: Restricted existential specialization, using implicit substitution in both directions. (Contributed by Zhi Wang, 28-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		rspceb2dv.1	$$⊢\left(\phi \wedge x\in B\right)\to \left(\psi \to \chi \right)$$
2		rspceb2dv.2	$$⊢\left(\phi \wedge \chi \right)\to A\in B$$
3		rspceb2dv.3	$$⊢\left(\phi \wedge \chi \right)\to \theta$$
4		rspceb2dv.4	$$⊢x=A\to \left(\psi \leftrightarrow \theta \right)$$
5	1	rexlimdva	$$⊢\phi \to \left(\exists x\in B\psi \to \chi \right)$$
6	4 2 3	rspcedvdw	$$⊢\left(\phi \wedge \chi \right)\to \exists x\in B\psi$$
7	6	ex	$$⊢\phi \to \left(\chi \to \exists x\in B\psi \right)$$
8	5 7	impbid	$$⊢\phi \to \left(\exists x\in B\psi \leftrightarrow \chi \right)$$