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	rspcev	$$⊢\left(A\in B\wedge \theta \right)\to \exists x\in B\psi$$
7	2 3 6	syl2anc	$$⊢\left(\phi \wedge \chi \right)\to \exists x\in B\psi$$
8	7	ex	$$⊢\phi \to \left(\chi \to \exists x\in B\psi \right)$$
9	5 8	impbid	$$⊢\phi \to \left(\exists x\in B\psi \leftrightarrow \chi \right)$$