MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfsb Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 axc16nf 2227 . 2 (∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
2 nfsb.1 . . 3 𝑧𝜑
32nfsb4 2494 . 2 (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
41, 3pm2.61i 183 1 𝑧[𝑦 / 𝑥]𝜑
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator