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

Theorem sbf 2147
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 2146 . 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 186   F/wnf 1639   [wsb 1765
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-12 1880  ax-13 2028
This theorem depends on definitions:  df-bi 187  df-an 371  df-ex 1636  df-nf 1640  df-sb 1766
This theorem is referenced by:  sbh  2148  sbf2  2149  nfs1f  2150  sb6x  2151  sbequ5  2154  sbequ6  2155  sbrim  2163  sblim  2164  sbrbif  2173  sbie  2175  sbieOLD  2176  sbid2  2181  equsb3  2202  sbcom4  2216  sbabel  2598  sbabelOLD  2599  nfcdeq  3276  mo5f  27811  iuninc  27871  suppss2f  27933  fmptdF  27950  disjdsct  27978  esumpfinvalf  28536  measiuns  28678  ballotlemodife  28955  bj-sbf3  30987  bj-sbf4  30988  mptsnunlem  31267  wl-equsb3  31384  ellimcabssub0  37004
  Copyright terms: Public domain W3C validator