Theorem nfsb 2552

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

This proof depends on syntax axioms:  ⊤wtru 1570  Ⅎwnf 1815  [wsb 2098

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-10 2177  ax-11 2193  ax-12 2212  ax-13 2401

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099

This theorem is used by:  hbsb  2553  sb10f  2556  2sb8e  2559  sb8eu  2625  cbvralf  3345  cbvralsv  3351  cbvrexsv  3352  cbvreu  3404  cbvrab  3449  cbvreucsf  3891  cbvrabcsf  3892  cbvopab1g  5179  cbvmptfg  5205  cbviota  6505  sb8iota  6507  cbvriota  7392  2sb5nd  45650