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

Theorem sbf 2408
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 2407 . 2 (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑𝜑))
31, 2ax-mp 5 1 ([𝑦 / 𝑥]𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wnf 1748  [wsb 1937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087  ax-13 2282
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-nf 1750  df-sb 1938
This theorem is referenced by:  sbh  2409  sbf2  2410  nfs1f  2411  sb6x  2412  sbequ5  2415  sbequ6  2416  sbrim  2424  sblim  2425  sbrbif  2434  sbie  2436  sbid2  2441  equsb3  2460  sbcom4  2474  sbabel  2822  nfcdeq  3465  mo5f  29452  iuninc  29505  suppss2f  29567  fmptdF  29584  disjdsct  29608  esumpfinvalf  30266  measiuns  30408  ballotlemodife  30687  bj-sbf3  32951  bj-sbf4  32952  mptsnunlem  33315  wl-equsb3  33467  ellimcabssub0  40167
  Copyright terms: Public domain W3C validator