Theorem rspcef

Description: Restricted existential specialization, using implicit substitution. (Contributed by Glauco Siliprandi, 24-Dec-2020)

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

Proof

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