Metamath Proof Explorer


Theorem nfsbv

Description: If z is not free in ph , it is not free in [ y / x ] ph when z is distinct from x and y . Version of nfsb requiring more disjoint variables, but fewer axioms. (Contributed by Mario Carneiro, 11-Aug-2016) (Revised by Wolf Lammen, 7-Feb-2023) Remove disjoint variable condition on x , y . (Revised by Steven Nguyen, 13-Aug-2023)

Ref Expression
Hypothesis nfsbv.nf 𝑧 𝜑
Assertion nfsbv 𝑧 [ 𝑦 / 𝑥 ] 𝜑

Proof

Step Hyp Ref Expression
1 nfsbv.nf 𝑧 𝜑
2 df-sb ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑤 ( 𝑤 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑤𝜑 ) ) )
3 nfv 𝑧 𝑤 = 𝑦
4 nfv 𝑧 𝑥 = 𝑤
5 4 1 nfim 𝑧 ( 𝑥 = 𝑤𝜑 )
6 5 nfal 𝑧𝑥 ( 𝑥 = 𝑤𝜑 )
7 3 6 nfim 𝑧 ( 𝑤 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑤𝜑 ) )
8 7 nfal 𝑧𝑤 ( 𝑤 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑤𝜑 ) )
9 2 8 nfxfr 𝑧 [ 𝑦 / 𝑥 ] 𝜑