Metamath Proof Explorer

Theorem spcgv

Description: Rule of specialization, using implicit substitution. Compare Theorem 7.3 of Quine p. 44. (Contributed by NM, 22-Jun-1994) Avoid ax-10 , ax-11 . (Revised by Wolf Lammen, 25-Aug-2023)

Ref Expression
Hypothesis spcgv.1 x = A φ ψ
Assertion spcgv A V x φ ψ


Step Hyp Ref Expression
1 spcgv.1 x = A φ ψ
2 elex A V A V
3 id A V A V
4 1 adantl A V x = A φ ψ
5 3 4 spcdv A V x φ ψ
6 2 5 syl A V x φ ψ