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 𝑧 𝜑
Assertion nfsbvOLD 𝑧 [ 𝑦 / 𝑥 ] 𝜑

Proof

Step Hyp Ref Expression
1 nfsbv.nf 𝑧 𝜑
2 sb6 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) )
3 nfv 𝑧 𝑥 = 𝑦
4 3 1 nfim 𝑧 ( 𝑥 = 𝑦𝜑 )
5 4 nfal 𝑧𝑥 ( 𝑥 = 𝑦𝜑 )
6 2 5 nfxfr 𝑧 [ 𝑦 / 𝑥 ] 𝜑