Theorem rspesbcd

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

	Ref	Expression
Hypotheses	rspesbcd.1	|- ( ph -> A e. B )
	rspesbcd.2	|- ( ph -> [. A / x ]. ps )
Assertion	rspesbcd	|- ( ph -> E. x e. B ps )

Proof

Step	Hyp	Ref	Expression
1		rspesbcd.1	|- ( ph -> A e. B )
2		rspesbcd.2	|- ( ph -> [. A / x ]. ps )
3		sbcel1v	|- ( [. A / x ]. x e. B <-> A e. B )
4	1 3	sylibr	|- ( ph -> [. A / x ]. x e. B )
5		sbcan	|- ( [. A / x ]. ( x e. B /\ ps ) <-> ( [. A / x ]. x e. B /\ [. A / x ]. ps ) )
6	4 2 5	sylanbrc	|- ( ph -> [. A / x ]. ( x e. B /\ ps ) )
7	6	spesbcd	|- ( ph -> E. x ( x e. B /\ ps ) )
8		df-rex	|- ( E. x e. B ps <-> E. x ( x e. B /\ ps ) )
9	7 8	sylibr	|- ( ph -> E. x e. B ps )