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

Theorem sbf 2180
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  |-  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 2179 . 2  |-  ( F/ x ph  ->  ( [ y  /  x ] ph  <->  ph ) )
31, 2ax-mp 5 1  |-  ( [ y  /  x ] ph 
<-> 
ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187   F/wnf 1661   [wsb 1790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-12 1909  ax-13 2058
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658  df-nf 1662  df-sb 1791
This theorem is referenced by:  sbh  2181  sbf2  2182  nfs1f  2183  sb6x  2184  sbequ5  2187  sbequ6  2188  sbrim  2196  sblim  2197  sbrbif  2206  sbie  2208  sbid2  2213  equsb3  2233  sbcom4  2247  sbabel  2592  sbabelOLD  2593  nfcdeq  3234  mo5f  28057  iuninc  28117  suppss2fOLD  28178  suppss2f  28179  fmptdF  28196  disjdsct  28224  esumpfinvalf  28844  measiuns  28986  ballotlemodife  29277  bj-sbf3  31350  bj-sbf4  31351  bj-sbieOLD  31356  mptsnunlem  31647  wl-equsb3  31791  ellimcabssub0  37580
  Copyright terms: Public domain W3C validator