Theorem rspc

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005) (Revised by Mario Carneiro, 11-Oct-2016)

	Ref	Expression
Hypotheses	rspc.1	|- F/ x ps
	rspc.2	|- ( x = A -> ( ph <-> ps ) )
Assertion	rspc	|- ( A e. B -> ( A. x e. B ph -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		rspc.1	|- F/ x ps
2		rspc.2	|- ( x = A -> ( ph <-> ps ) )
3		df-ral	|- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
4		nfcv	|- F/_ x A
5		nfv	|- F/ x A e. B
6	5 1	nfim	|- F/ x ( A e. B -> ps )
7		eleq1	|- ( x = A -> ( x e. B <-> A e. B ) )
8	7 2	imbi12d	|- ( x = A -> ( ( x e. B -> ph ) <-> ( A e. B -> ps ) ) )
9	4 6 8	spcgf	|- ( A e. B -> ( A. x ( x e. B -> ph ) -> ( A e. B -> ps ) ) )
10	9	pm2.43a	|- ( A e. B -> ( A. x ( x e. B -> ph ) -> ps ) )
11	3 10	biimtrid	|- ( A e. B -> ( A. x e. B ph -> ps ) )