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

Theorem nfsb 2577
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
StepHypRef Expression
1 axc16nf 2284 . 2 (∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
2 nfsb.1 . . 3 𝑧𝜑
32nfsb4 2527 . 2 (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
41, 3pm2.61i 176 1 𝑧[𝑦 / 𝑥]𝜑
Colors of variables: wff setvar class
Syntax hints:  wal 1630  wnf 1857  [wsb 2046
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047
This theorem is referenced by:  hbsb  2578  sb10f  2593  2sb8e  2604  sb8eu  2641  2mo  2689  cbvralf  3304  cbvreu  3308  cbvralsv  3321  cbvrexsv  3322  cbvrab  3338  cbvreucsf  3708  cbvrabcsf  3709  cbvopab1  4875  cbvmptf  4900  cbvmpt  4901  ralxpf  5424  cbviota  6017  sb8iota  6019  cbvriota  6785  dfoprab4f  7394  mo5f  29654  ax11-pm2  33151  2sb5nd  39296
  Copyright terms: Public domain W3C validator