Theorem nfsb 2521

Description: If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. See nfsbv 2322 for a version with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2370. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Feb-2024.) Usage of this theorem is discouraged because it depends on ax-13 2370. Use nfsbv 2322 instead. (New usage is discouraged.)

Hypothesis

Ref	Expression
nfsb.1	⊢ Ⅎ𝑧𝜑

Assertion

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

Distinct variable group:   𝑦,𝑧

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

Proof of Theorem nfsb

Step	Hyp	Ref	Expression
1		nftru 1805	. . 3 ⊢ Ⅎ𝑥⊤
2		nfsb.1	. . . 4 ⊢ Ⅎ𝑧𝜑
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑧𝜑)
4	1, 3	nfsbd 2520	. 2 ⊢ (⊤ → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
5	4	mptru 1547	1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1784  [wsb 2066

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 1912  ax-6 1970  ax-7 2010  ax-10 2136  ax-11 2153  ax-12 2170  ax-13 2370

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-nf 1785  df-sb 2067

This theorem is referenced by:  hbsb  2522  sb10f  2525  2sb8e  2528  sb8eu  2593  cbvralf  3355  cbvralsv  3361  cbvrexsv  3362  cbvreu  3423  cbvrab  3472  cbvreucsf  3940  cbvrabcsf  3941  cbvopab1g  5224  cbvmptfg  5258  cbviota  6505  sb8iota  6507  cbvriota  7382  2sb5nd  43624