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

Theorem sbf 2273
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 2099. (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 2272 . 2 (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑𝜑))
31, 2ax-mp 5 1 ([𝑦 / 𝑥]𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 209  wnf 1785  [wsb 2070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-12 2179
This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786  df-sb 2071
This theorem is referenced by:  sbf2  2274  sbh  2275  nfs1f  2277  sbbibOLD  2291  sbrim  2315  sblim  2317  sbrbif  2323  sbievOLD  2333  sb6x  2489  sbequ5  2490  sbequ6  2491  sb2ae  2538  sbie  2546  sbid2  2552  sbabel  3013  nfcdeq  3754  mo5f  30265  suppss2f  30398  fmptdF  30415  disjdsct  30452  esumpfinvalf  31395  bj-sbf3  34224  bj-sbf4  34225  ellimcabssub0  42189  2reu8i  43599  ichf  43897
  Copyright terms: Public domain W3C validator