Theorem nfsb 2528

Description: If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. See nfsbv 2336 for a version with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2377. (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 2377. Use nfsbv 2336 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 1806	. . 3 ⊢ Ⅎ𝑥⊤
2		nfsb.1	. . . 4 ⊢ Ⅎ𝑧𝜑
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑧𝜑)
4	1, 3	nfsbd 2527	. 2 ⊢ (⊤ → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
5	4	mptru 1549	1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1785  [wsb 2068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-10 2147  ax-11 2163  ax-12 2185  ax-13 2377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069

This theorem is referenced by:  hbsb  2529  sb10f  2532  2sb8e  2535  sb8eu  2601  cbvralf  3332  cbvralsv  3338  cbvrexsv  3339  cbvreu  3393  cbvrab  3441  cbvreucsf  3895  cbvrabcsf  3896  cbvopab1g  5175  cbvmptfg  5201  cbviota  6465  sb8iota  6467  cbvriota  7338  2sb5nd  44913