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 φ x y x φ


Step Hyp Ref Expression
1 nfs1v x y x φ
2 1 nf5ri y x φ x y x φ