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

Theorem sbf 2527
 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 2526 . 2 (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑𝜑))
31, 2ax-mp 5 1 ([𝑦 / 𝑥]𝜑𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196  Ⅎwnf 1856  [wsb 2049 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-12 2203  ax-13 2408 This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-nf 1858  df-sb 2050 This theorem is referenced by:  sbh  2528  sbf2  2529  nfs1f  2530  sb6x  2531  sbequ5  2534  sbequ6  2535  sbrim  2543  sblim  2544  sbrbif  2553  sbie  2555  sbid2  2560  equsb3  2580  elsb3  2583  elsb4  2586  sbcom4  2594  sbabel  2942  nfcdeq  3584  mo5f  29664  iuninc  29717  suppss2f  29779  fmptdF  29796  disjdsct  29820  esumpfinvalf  30478  measiuns  30620  ballotlemodife  30899  bj-sbf3  33161  bj-sbf4  33162  mptsnunlem  33522  wl-equsb3  33672  ellimcabssub0  40367
 Copyright terms: Public domain W3C validator