Metamath Proof Explorer


Theorem wl-nfs1t

Description: If y is not free in ph , x is not free in [ y / x ] ph . Closed form of nfs1 . (Contributed by Wolf Lammen, 27-Jul-2019)

Ref Expression
Assertion wl-nfs1t yφxyxφ

Proof

Step Hyp Ref Expression
1 sbequ12r y=xyxφφ
2 1 equcoms x=yyxφφ
3 2 sps xx=yyxφφ
4 3 drnf1 xx=yxyxφyφ
5 4 biimprd xx=yyφxyxφ
6 nfsb2 ¬xx=yxyxφ
7 6 a1d ¬xx=yyφxyxφ
8 5 7 pm2.61i yφxyxφ