Theorem nfsbv 2349

Description: If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is distinct from 𝑥 and 𝑦. Version of nfsb 2565 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 𝑥, 𝑦. (Revised by Steven Nguyen, 13-Aug-2023.)

Hypothesis

Ref	Expression
nfsbv.nf	⊢ Ⅎ𝑧𝜑

Assertion

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

Distinct variable groups:   𝑥,𝑧   𝑦,𝑧

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

Proof of Theorem nfsbv

Dummy variable 𝑤 is distinct from all other variables.

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

Syntax hints:   → wi 4  ∀wal 1535  Ⅎwnf 1784  [wsb 2069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2145  ax-11 2161  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070

This theorem is referenced by:  hbsbw  2351  sbco2v  2352  2sb8ev  2375  sb8euv  2685  2mo  2733  nfcrii  2972  cbvralfw  3439  cbvreuw  3445  cbvrabw  3491  cbvrabcsfw  3926  cbvopab1  5141  cbvmptf  5167  ralxpf  5719  cbviotaw  6323  cbvriotaw  7125  dfoprab4f  7756  mo5f  30255  ax11-pm2  34161  dfich2  43620  dfich2ai  43621  ichbi12i  43625