Theorem nfsb 2468

Description: If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfsb.1	⊢ Ⅎ𝑧𝜑

Assertion

Ref	Expression
nfsb	⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑

Distinct variable group:   𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem nfsb

Step	Hyp	Ref	Expression
1		axc16nf 2175	. 2 ⊢ (∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
2		nfsb.1	. . 3 ⊢ Ⅎ𝑧𝜑
3	2	nfsb4 2418	. 2 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
4	1, 3	pm2.61i 176	1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑

Syntax hints:  ∀wal 1521  Ⅎwnf 1748  [wsb 1937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938

This theorem is referenced by:  hbsb  2469  sb10f  2484  2sb8e  2495  sb8eu  2532  2mo  2580  cbvralf  3195  cbvreu  3199  cbvralsv  3212  cbvrexsv  3213  cbvrab  3229  cbvreucsf  3600  cbvrabcsf  3601  cbvopab1  4756  cbvmptf  4781  cbvmpt  4782  ralxpf  5301  cbviota  5894  sb8iota  5896  cbvriota  6661  dfoprab4f  7270  mo5f  29452  ax11-pm2  32948  2sb5nd  39093