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

Theorem sbf 1966
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 1965 . 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 1531   [wsb 1629
This theorem is referenced by:  sbh  1967  sbf2  1968  sb6x  1969  nfs1f  1970  sbequ5  1971  sbequ6  1972  sbt  1973  sbrim  2007  sblim  2008  sbrbif  2014  sbid2  2024  sbabel  2445  nfcdeq  2988  ballotlemodife  23056  mo5f  23143  iuninc  23158  suppss2f  23201  fmptdF  23221  disjdsct  23369  esumpfinvalf  23444  measiuns  23544
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-sb 1630
  Copyright terms: Public domain W3C validator