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

Theorem sbf 2257
Description: Substitution for a variable not free in a wff does not affect it. For a version requiring disjoint variables but fewer axioms, see sbv 2083. (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 2256 . 2 (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑𝜑))
31, 2ax-mp 5 1 ([𝑦 / 𝑥]𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wnf 1777  [wsb 2059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2166
This theorem depends on definitions:  df-bi 206  df-ex 1774  df-nf 1778  df-sb 2060
This theorem is referenced by:  sbf2  2258  sbh  2259  nfs1f  2261  sbrimOLD  2294  sblim  2295  sbrbif  2300  sb8f  2343  sb6x  2457  sbequ5  2458  sbequ6  2459  sb2ae  2489  sbie  2495  sbid2  2501  sbabel  2927  sbabelOLD  2928  sbhypf  3528  nfcdeq  3769  mo5f  32365  suppss2f  32505  fmptdF  32523  disjdsct  32564  esumpfinvalf  33826  bj-sbf3  36447  bj-sbf4  36448  ellimcabssub0  45143  2reu8i  46631  ichf  46927
  Copyright terms: Public domain W3C validator