Theorem nfsbv 2328

Description: If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is disjoint from both 𝑥 and 𝑦. Version of nfsb 2527 with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2372. (Contributed by Mario Carneiro, 11-Aug-2016.) (Revised by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on 𝑥, 𝑦. (Revised by Steven Nguyen, 13-Aug-2023.) (Proof shortened by Wolf Lammen, 25-Oct-2024.)

Hypothesis

Ref	Expression
nfsbv.nf	⊢ Ⅎ𝑧𝜑

Assertion

Ref	Expression
nfsbv	⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑

Distinct variable groups:   𝑥,𝑧   𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem nfsbv

Step	Hyp	Ref	Expression
1		nfsbv.nf	. . . 4 ⊢ Ⅎ𝑧𝜑
2	1	nf5ri 2191	. . 3 ⊢ (𝜑 → ∀𝑧𝜑)
3	2	hbsbw 2171	. 2 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑)
4	3	nf5i 2144	1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1787  [wsb 2068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2139  ax-11 2156  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-nf 1788  df-sb 2069

This theorem is referenced by:  hbsbwOLD  2330  sbco2v  2331  2sb8ev  2354  sb8euv  2599  2mo  2650  nfcriiOLD  2899  cbvralfwOLD  3359  cbvreuw  3365  cbvrabw  3414  cbvrabcsfw  3872  cbvopab1  5145  cbvmptf  5179  ralxpf  5744  cbviotaw  6383  cbvriotaw  7221  dfoprab4f  7869  mo5f  30738  ax11-pm2  34946  dfich2  44798  ichbi12i  44800