This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 -> ( ph <-> ps ) )
Assertion spcgv 
|- ( A e. V -> ( A. x ph -> ps ) )

Proof

Step Hyp Ref Expression
1 spcgv.1 
 |-  ( x = A -> ( ph <-> ps ) )
2 elex 
 |-  ( A e. V -> A e. _V )
3 id 
 |-  ( A e. _V -> A e. _V )
4 1 adantl 
 |-  ( ( A e. _V /\ x = A ) -> ( ph <-> ps ) )
5 3 4 spcdv 
 |-  ( A e. _V -> ( A. x ph -> ps ) )
6 2 5 syl 
 |-  ( A e. V -> ( A. x ph -> ps ) )