Metamath Proof Explorer


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 xψ
rspc.2 x=Aφψ
Assertion rspc ABxBφψ

Proof

Step Hyp Ref Expression
1 rspc.1 xψ
2 rspc.2 x=Aφψ
3 df-ral xBφxxBφ
4 nfcv _xA
5 nfv xAB
6 5 1 nfim xABψ
7 eleq1 x=AxBAB
8 7 2 imbi12d x=AxBφABψ
9 4 6 8 spcgf ABxxBφABψ
10 9 pm2.43a ABxxBφψ
11 3 10 syl5bi ABxBφψ