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 -> ( ps <-> ch ) )
	rspcedvdw.1	|- ( ph -> A e. B )
	rspcedvdw.2	|- ( ph -> ch )
Assertion	rspcedvdw	|- ( ph -> E. x e. B ps )

Proof

Step	Hyp	Ref	Expression
1		rspcedvdw.s	|- ( x = A -> ( ps <-> ch ) )
2		rspcedvdw.1	|- ( ph -> A e. B )
3		rspcedvdw.2	|- ( ph -> ch )
4	1	rspcev	|- ( ( A e. B /\ ch ) -> E. x e. B ps )
5	2 3 4	syl2anc	|- ( ph -> E. x e. B ps )