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

Theorem sbf 2083
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 2081 . 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 177   F/wnf 1550   [wsb 1655
This theorem is referenced by:  sbh  2084  sbf2  2085  sb6x  2086  nfs1f  2087  sbequ5  2088  sbequ6  2089  sbt  2090  sbrim  2124  sblim  2125  sbrbif  2131  sbid2  2141  pm11.07  2172  sbabel  2574  nfcdeq  3126  mo5f  23933  iuninc  23972  suppss2f  24010  fmptdF  24030  disjdsct  24051  esumpfinvalf  24427  measiuns  24532  ballotlemodife  24716
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757  ax-12 1946
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-sb 1656
  Copyright terms: Public domain W3C validator