Theorem rspesbcd

Description: Restricted quantifier version of spesbcd . (Contributed by Eric Schmidt, 29-Sep-2025)

	Ref	Expression
Hypotheses	rspesbcd.1	$$⊢\phi \to A\in B$$
	rspesbcd.2	$$⊢\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi$$
Assertion	rspesbcd	$$⊢\phi \to \exists x\in B\psi$$

Proof

Step	Hyp	Ref	Expression
1		rspesbcd.1	$$⊢\phi \to A\in B$$
2		rspesbcd.2	$$⊢\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi$$
3		sbcel1v	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}x\in B\leftrightarrow A\in B$$
4	1 3	sylibr	$$⊢\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}x\in B$$
5		sbcan	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(x\in B\wedge \psi \right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}x\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)$$
6	4 2 5	sylanbrc	$$⊢\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(x\in B\wedge \psi \right)$$
7	6	spesbcd	$$⊢\phi \to \exists x\left(x\in B\wedge \psi \right)$$
8		df-rex	$$⊢\exists x\in B\psi \leftrightarrow \exists x\left(x\in B\wedge \psi \right)$$
9	7 8	sylibr	$$⊢\phi \to \exists x\in B\psi$$