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

Theorem sbf 2119
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 2117 . 2  |-  ( F/ x ph  ->  ( [ y  /  x ] ph  <->  ph ) )
31, 2ax-mp 5 1  |-  ( [ y  /  x ] ph 
<-> 
ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   F/wnf 1554   [wsb 1659
This theorem is referenced by:  sbh  2120  sbf2  2121  nfs1f  2122  sb6x  2123  sbequ5  2126  sbequ6  2127  sbtOLD  2128  sbrim  2138  sblim  2139  sbrbif  2148  sbieALT  2153  sbid2  2161  pm11.07  2193  sbabel  2600  nfcdeq  3160  mo5f  23977  iuninc  24016  suppss2f  24054  fmptdF  24074  disjdsct  24095  esumpfinvalf  24471  measiuns  24576  ballotlemodife  24760  ax7w17lem1AUX7  29749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762  ax-12 1951
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555  df-sb 1660
  Copyright terms: Public domain W3C validator