Description: A weak form of specialization. Lemma 8 of KalishMontague p. 87. Uses only Tarski's FOL axiom schemes. For stronger forms using more axioms, see spimv and spimfv . (Contributed by NM, 9Apr2017)
Ref  Expression  

Hypothesis  spimvw.1   ( x = y > ( ph > ps ) ) 

Assertion  spimvw   ( A. x ph > ps ) 
Step  Hyp  Ref  Expression 

1  spimvw.1   ( x = y > ( ph > ps ) ) 

2  ax5   ( . ps > A. x . ps ) 

3  2 1  spimw   ( A. x ph > ps ) 