Description: The setvar x is not free in [ y / x ] ph when x and y are distinct. (Contributed by NM, 26May1993)
Ref  Expression  

Assertion  hbs1   ( [ y / x ] ph > A. x [ y / x ] ph ) 
Step  Hyp  Ref  Expression 

1  nfs1v   F/ x [ y / x ] ph 

2  1  nf5ri   ( [ y / x ] ph > A. x [ y / x ] ph ) 