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

Theorem sbf 2367
Description: Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
Hypothesis
Ref Expression
sbf.1 𝑥𝜑
Assertion
Ref Expression
sbf ([𝑦 / 𝑥]𝜑𝜑)

Proof of Theorem sbf
StepHypRef Expression
1 sbf.1 . 2 𝑥𝜑
2 sbft 2366 . 2 (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑𝜑))
31, 2ax-mp 5 1 ([𝑦 / 𝑥]𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wnf 1698  [wsb 1866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2033  ax-13 2233
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-nf 1700  df-sb 1867
This theorem is referenced by:  sbh  2368  sbf2  2369  nfs1f  2370  sb6x  2371  sbequ5  2374  sbequ6  2375  sbrim  2383  sblim  2384  sbrbif  2393  sbie  2395  sbid2  2400  equsb3  2419  sbcom4  2433  sbabel  2778  nfcdeq  3398  mo5f  28542  iuninc  28595  suppss2f  28653  fmptdF  28670  disjdsct  28697  esumpfinvalf  29299  measiuns  29441  ballotlemodife  29720  bj-sbf3  31848  bj-sbf4  31849  bj-sbieOLD  31854  mptsnunlem  32185  wl-equsb3  32340  ellimcabssub0  38508
  Copyright terms: Public domain W3C validator