Description: The setvar x is not free in [ y / x ] ph when x and y are distinct. (Contributed by Mario Carneiro, 11Aug2016) Shorten nfs1v and hbs1 combined. (Revised by Wolf Lammen, 28Jul2022)
Ref  Expression  

Assertion  nfs1v   F/ x [ y / x ] ph 
Step  Hyp  Ref  Expression 

1  sb6   ( [ y / x ] ph <> A. x ( x = y > ph ) ) 

2  nfa1   F/ x A. x ( x = y > ph ) 

3  1 2  nfxfr   F/ x [ y / x ] ph 