Theorem nfsbv 2318

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

Syntax hints:  Ⅎwnf 1778  [wsb 2060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-10 2130  ax-11 2147  ax-12 2164

This theorem depends on definitions:  df-bi 206  df-ex 1775  df-nf 1779  df-sb 2061

This theorem is referenced by:  hbsbwOLD  2320  sbco2v  2321  2sb8ef  2347  sb8euv  2588  2mo  2639  nfcriiOLD  2891  cbvralfwOLD  3315  cbvreuwOLD  3407  cbvrabw  3462  cbvrabcsfw  3933  cbvopab1  5217  cbvmptf  5251  ralxpf  5843  cbviotaw  6501  cbvriotaw  7379  dfoprab4f  8052  mo5f  32260  ax11-pm2  36236  dfich2  46711  ichbi12i  46713