Theorem nfsb 2526

Description: If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. Usage of this theorem is discouraged because it depends on ax-13 2371. For a version requiring more disjoint variables, but fewer axioms, see nfsbv 2331. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Feb-2024.) (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 1812	. . 3 ⊢ Ⅎ𝑥⊤
2		nfsb.1	. . . 4 ⊢ Ⅎ𝑧𝜑
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑧𝜑)
4	1, 3	nfsbd 2525	. 2 ⊢ (⊤ → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
5	4	mptru 1550	1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑

Syntax hints:  ⊤wtru 1544  Ⅎwnf 1791  [wsb 2072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-10 2143  ax-11 2160  ax-12 2177  ax-13 2371

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2073

This theorem is referenced by:  hbsb  2528  sb10f  2531  2sb8e  2534  sb8eu  2599  cbvralf  3337  cbvreu  3346  cbvralsv  3369  cbvrexsv  3370  cbvrab  3391  cbvreucsf  3845  cbvrabcsf  3846  cbvopab1g  5114  cbvmptfg  5140  cbviota  6326  sb8iota  6328  cbvriota  7162  2sb5nd  41794