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 1837	. . 3 ⊢ Ⅎ𝑥⊤
2		nfsb.1	. . . 4 ⊢ Ⅎ𝑧𝜑
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑧𝜑)
4	1, 3	nfsbd 2551	. 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 2178  ax-11 2194  ax-12 2213  ax-13 2401

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  2553  sb10f  2556  2sb8e  2559  sb8eu  2625  cbvralf  3345  cbvralsv  3351  cbvrexsv  3352  cbvreu  3404  cbvrab  3449  cbvreucsf  3891  cbvrabcsf  3892  cbvopab1g  5180  cbvmptfg  5206  cbviota  6498  sb8iota  6500  cbvriota  7383  2sb5nd  45383