Theorem rspcedvdw

Description: Version of rspcedvd where the implicit substitution hypothesis does not have an antecedent, which also avoids a disjoint variable condition on ph , x . (Contributed by SN, 20-Aug-2024)

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

Proof

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