Metamath Proof Explorer

Theorem hbs1

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

Ref Expression
Assertion hbs1 
|- ( [ y / x ] ph -> A. x [ y / x ] ph )

Proof

Step Hyp Ref Expression
1 nfs1v 
 |-  F/ x [ y / x ] ph
2 1 nf5ri 
 |-  ( [ y / x ] ph -> A. x [ y / x ] ph )