Theorem nfsb 2518

Description: If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. For a version requiring more disjoint variables, but fewer axioms, see nfsbv 2312. (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 2227	. 2 ⊢ (∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
2		nfsb.1	. . 3 ⊢ Ⅎ𝑧𝜑
3	2	nfsb4 2494	. 2 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
4	1, 3	pm2.61i 183	1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑

Syntax hints:  ∀wal 1520  Ⅎwnf 1765  [wsb 2042

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043

This theorem is referenced by:  hbsb  2519  sb10f  2524  2sb8e  2530  sb8eu  2652  cbvralf  3397  cbvreu  3401  cbvralsv  3415  cbvrexsv  3416  cbvrab  3433  cbvreucsf  3851  cbvrabcsf  3852  cbvopab1  5035  cbvmptf  5059  cbvmpt  5060  ralxpf  5603  cbviota  6194  sb8iota  6196  cbvriota  6987  dfoprab4f  7610  mo5f  29945  ax11-pm2  33729  2sb5nd  40433  dfich2  43095  dfich2ai  43096  dfich2OLD  43098  ichbi12i  43100