Theorem nfsb 2555

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

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

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 1945  ax-6 2002  ax-7 2043  ax-10 2180  ax-11 2197  ax-12 2216  ax-13 2404

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 2102

This theorem is used by:  hbsb  2556  sb10f  2559  2sb8e  2562  sb8eu  2628  cbvralf  3349  cbvralsv  3355  cbvrexsv  3356  cbvreu  3408  cbvrab  3453  cbvreucsf  3895  cbvrabcsf  3896  cbvopab1g  5186  cbvmptfg  5212  cbviota  6529  sb8iota  6531  cbvriota  7421  2sb5nd  45803