Theorem rspcedvd

Description: Restricted existential specialization, using implicit substitution. Variant of rspcedv . (Contributed by AV, 27-Nov-2019)

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

Proof

Step	Hyp	Ref	Expression
1		rspcedvd.1	|- ( ph -> A e. B )
2		rspcedvd.2	|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )
3		rspcedvd.3	|- ( ph -> ch )
4	1 2	rspcedv	|- ( ph -> ( ch -> E. x e. B ps ) )
5	3 4	mpd	|- ( ph -> E. x e. B ps )