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

Theorem sbf 2031
Description: Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
Hypothesis
Ref Expression
sbf.1  |-  F/ x ph
Assertion
Ref Expression
sbf  |-  ( [ y  /  x ] ph 
<-> 
ph )

Proof of Theorem sbf
StepHypRef Expression
1 sbf.1 . 2  |-  F/ x ph
2 sbft 2030 . 2  |-  ( F/ x ph  ->  ( [ y  /  x ] ph  <->  ph ) )
31, 2ax-mp 8 1  |-  ( [ y  /  x ] ph 
<-> 
ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   F/wnf 1544   [wsb 1648
This theorem is referenced by:  sbh  2032  sbf2  2033  sb6x  2034  nfs1f  2035  sbequ5  2036  sbequ6  2037  sbt  2038  sbrim  2072  sblim  2073  sbrbif  2079  sbid2  2089  sbabel  2520  nfcdeq  3064  mo5f  23167  iuninc  23210  suppss2f  23253  fmptdF  23272  disjdsct  23294  esumpfinvalf  23732  measiuns  23835  ballotlemodife  24004
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-sb 1649
  Copyright terms: Public domain W3C validator