Theorem rspcimdv

Description: Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		rspcimdv.1	|- ( ph -> A e. B )
2		rspcimdv.2	|- ( ( ph /\ x = A ) -> ( ps -> ch ) )
3		df-ral	|- ( A. x e. B ps <-> A. x ( x e. B -> ps ) )
4		simpr	|- ( ( ph /\ x = A ) -> x = A )
5	4	eleq1d	|- ( ( ph /\ x = A ) -> ( x e. B <-> A e. B ) )
6	5	biimprd	|- ( ( ph /\ x = A ) -> ( A e. B -> x e. B ) )
7	6 2	imim12d	|- ( ( ph /\ x = A ) -> ( ( x e. B -> ps ) -> ( A e. B -> ch ) ) )
8	1 7	spcimdv	|- ( ph -> ( A. x ( x e. B -> ps ) -> ( A e. B -> ch ) ) )
9	1 8	mpid	|- ( ph -> ( A. x ( x e. B -> ps ) -> ch ) )
10	3 9	biimtrid	|- ( ph -> ( A. x e. B ps -> ch ) )