Metamath Proof Explorer


Theorem nfs1v

Description: The setvar x is not free in [ y / x ] ph when x and y are distinct. (Contributed by Mario Carneiro, 11-Aug-2016) Shorten nfs1v and hbs1 combined. (Revised by Wolf Lammen, 28-Jul-2022)

Ref Expression
Assertion nfs1v
|- F/ x [ y / x ] ph

Proof

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