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

Theorem sbf 2378
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 2377 . 2 (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑𝜑))
31, 2ax-mp 5 1 ([𝑦 / 𝑥]𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wnf 1706  [wsb 1878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-12 2045  ax-13 2244
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-nf 1708  df-sb 1879
This theorem is referenced by:  sbh  2379  sbf2  2380  nfs1f  2381  sb6x  2382  sbequ5  2385  sbequ6  2386  sbrim  2394  sblim  2395  sbrbif  2404  sbie  2406  sbid2  2411  equsb3  2430  sbcom4  2444  sbabel  2790  nfcdeq  3426  mo5f  29296  iuninc  29351  suppss2f  29412  fmptdF  29429  disjdsct  29454  esumpfinvalf  30112  measiuns  30254  ballotlemodife  30533  bj-sbf3  32801  bj-sbf4  32802  mptsnunlem  33156  wl-equsb3  33308  ellimcabssub0  39649
  Copyright terms: Public domain W3C validator