Metamath Proof Explorer


Theorem rspcimedv

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

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

Proof

Step Hyp Ref Expression
1 rspcimdv.1 φAB
2 rspcimedv.2 φx=Aχψ
3 2 con3d φx=A¬ψ¬χ
4 1 3 rspcimdv φxB¬ψ¬χ
5 4 con2d φχ¬xB¬ψ
6 dfrex2 xBψ¬xB¬ψ
7 5 6 syl6ibr φχxBψ