Theorem rspced

Description: Restricted existential specialization, using implicit substitution. (Contributed by Glauco Siliprandi, 15-Feb-2025)

	Ref	Expression
Hypotheses	rspced.1	|- F/ x ch
	rspced.2	|- F/_ x A
	rspced.3	|- F/_ x B
	rspced.4	|- ( ph -> A e. B )
	rspced.5	|- ( ph -> ch )
	rspced.6	|- ( x = A -> ( ps <-> ch ) )
Assertion	rspced	|- ( ph -> E. x e. B ps )

Proof

Step	Hyp	Ref	Expression
1		rspced.1	|- F/ x ch
2		rspced.2	|- F/_ x A
3		rspced.3	|- F/_ x B
4		rspced.4	|- ( ph -> A e. B )
5		rspced.5	|- ( ph -> ch )
6		rspced.6	|- ( x = A -> ( ps <-> ch ) )
7	1 2 3 6	rspcef	|- ( ( A e. B /\ ch ) -> E. x e. B ps )
8	4 5 7	syl2anc	|- ( ph -> E. x e. B ps )