Metamath Proof Explorer


Theorem rspcimdv

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

Ref Expression
Hypotheses rspcimdv.1 φAB
rspcimdv.2 φx=Aψχ
Assertion rspcimdv φxBψχ

Proof

Step Hyp Ref Expression
1 rspcimdv.1 φAB
2 rspcimdv.2 φx=Aψχ
3 df-ral xBψxxBψ
4 simpr φx=Ax=A
5 4 eleq1d φx=AxBAB
6 5 biimprd φx=AABxB
7 6 2 imim12d φx=AxBψABχ
8 1 7 spcimdv φxxBψABχ
9 1 8 mpid φxxBψχ
10 3 9 syl5bi φxBψχ