Metamath Proof Explorer


Theorem rspcevOLD

Description: Obsolete version of rspce as of 12-Dec-2023. Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 rspcv.1 x=Aφψ
2 nfv xψ
3 2 1 rspce ABψxBφ