Theorem nfsb 2557

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

This proof depends on syntax axioms:  ⊤wtru 1571  Ⅎwnf 1816  [wsb 2099

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-10 2179  ax-11 2195  ax-12 2216  ax-13 2406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100

This theorem is used by:  hbsb  2558  sb10f  2561  2sb8e  2564  sb8eu  2630  cbvralf  3351  cbvralsv  3357  cbvrexsv  3358  cbvreu  3410  cbvrab  3456  cbvreucsf  3898  cbvrabcsf  3899  cbvopab1g  5188  cbvmptfg  5214  cbviota  6505  sb8iota  6507  cbvriota  7386  2sb5nd  45302