Metamath Proof Explorer


Theorem nfsbOLD

Description: Obsolete version of nfsb as of 25-Feb-2024. (Contributed by Mario Carneiro, 11-Aug-2016) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis nfsb.1 𝑧 𝜑
Assertion nfsbOLD 𝑧 [ 𝑦 / 𝑥 ] 𝜑

Proof

Step Hyp Ref Expression
1 nfsb.1 𝑧 𝜑
2 axc16nf ( ∀ 𝑧 𝑧 = 𝑦 → Ⅎ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 )
3 1 nfsb4 ( ¬ ∀ 𝑧 𝑧 = 𝑦 → Ⅎ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 )
4 2 3 pm2.61i 𝑧 [ 𝑦 / 𝑥 ] 𝜑