Metamath Proof Explorer


Theorem nfsbvOLD

Description: Obsolete version of nfsbv as of 13-Aug-2023. (Contributed by Wolf Lammen, 7-Feb-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis nfsbv.nf
|- F/ z ph
Assertion nfsbvOLD
|- F/ z [ y / x ] ph

Proof

Step Hyp Ref Expression
1 nfsbv.nf
 |-  F/ z ph
2 sb6
 |-  ( [ y / x ] ph <-> A. x ( x = y -> ph ) )
3 nfv
 |-  F/ z x = y
4 3 1 nfim
 |-  F/ z ( x = y -> ph )
5 4 nfal
 |-  F/ z A. x ( x = y -> ph )
6 2 5 nfxfr
 |-  F/ z [ y / x ] ph