Metamath Proof Explorer


Theorem rspcev

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998) Drop ax-10 , ax-11 , ax-12 . (Revised by SN, 12-Dec-2023)

Ref Expression
Hypothesis rspcv.1 x=Aφψ
Assertion rspcev ABψxBφ

Proof

Step Hyp Ref Expression
1 rspcv.1 x=Aφψ
2 id ABAB
3 1 adantl ABx=Aφψ
4 2 3 rspcedv ABψxBφ
5 4 imp ABψxBφ