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

Theorem sbf 2263
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 2092. (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 2262 . 2 (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑𝜑))
31, 2ax-mp 5 1 ([𝑦 / 𝑥]𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wnf 1786  [wsb 2068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787  df-sb 2069
This theorem is referenced by:  sbf2  2264  sbh  2265  nfs1f  2267  sbrimOLD  2302  sblim  2303  sbrbif  2308  sb8f  2350  sb6x  2463  sbequ5  2464  sbequ6  2465  sb2ae  2499  sbie  2505  sbid2  2511  sbabel  2942  sbabelOLD  2943  sbhypf  3510  nfcdeq  3740  mo5f  31459  suppss2f  31595  fmptdF  31614  disjdsct  31658  esumpfinvalf  32715  bj-sbf3  35333  bj-sbf4  35334  ellimcabssub0  43932  2reu8i  45419  ichf  45716
  Copyright terms: Public domain W3C validator