Theorem nfsb 2553

Description: If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. See nfsbv 2361 for a version with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2402. (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 2402. Use nfsbv 2361 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 2552	. 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 2402

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  2554  sb10f  2557  2sb8e  2560  sb8eu  2626  cbvralf  3346  cbvralsv  3352  cbvrexsv  3353  cbvreu  3405  cbvrab  3450  cbvreucsf  3891  cbvrabcsf  3892  cbvopab1g  5180  cbvmptfg  5206  cbviota  6502  sb8iota  6504  cbvriota  7388  2sb5nd  45528