Theorem nfsbv 2319

Description: If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is disjoint from both 𝑥 and 𝑦. Version of nfsb 2522 with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2367. (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 2183	. . 3 ⊢ (𝜑 → ∀𝑧𝜑)
3	2	hbsbw 2164	. 2 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑)
4	3	nf5i 2137	1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1781  [wsb 2062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-10 2132  ax-11 2149  ax-12 2166

This theorem depends on definitions:  df-bi 206  df-ex 1778  df-nf 1782  df-sb 2063

This theorem is referenced by:  hbsbwOLD  2321  sbco2v  2322  2sb8ef  2349  sb8euv  2594  2mo  2645  nfcriiOLD  2895  cbvralfwOLD  3371  cbvreuwOLD  3379  cbvrabw  3426  cbvrabcsfw  3878  cbvopab1  5152  cbvmptf  5186  ralxpf  5759  cbviotaw  6406  cbvriotaw  7261  dfoprab4f  7916  mo5f  30865  ax11-pm2  35047  dfich2  44950  ichbi12i  44952