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

Theorem sbf 2199
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 2040. (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 2198 . 2 (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑𝜑))
31, 2ax-mp 5 1 ([𝑦 / 𝑥]𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 198  wnf 1746  [wsb 2015
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-12 2106
This theorem depends on definitions:  df-bi 199  df-ex 1743  df-nf 1747  df-sb 2016
This theorem is referenced by:  sbf2  2200  sbh  2201  nfs1f  2204  sbbibOLD  2215  sbrim  2238  sblim  2239  sbrbif  2244  sbievOLD  2254  sb6x  2402  sbequ5  2403  sbequ6  2404  sb2ae  2457  sbie  2468  sbid2  2474  sbabel  2966  nfcdeq  3677  mo5f  30035  suppss2f  30146  fmptdF  30163  disjdsct  30197  esumpfinvalf  30985  bj-sbf3  33659  bj-sbf4  33660  ellimcabssub0  41335  2reu8i  42724
  Copyright terms: Public domain W3C validator