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

Theorem sbequ12 1940
Description: An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
sbequ12  |-  ( x  =  y  ->  ( ph 
<->  [ y  /  x ] ph ) )

Proof of Theorem sbequ12
StepHypRef Expression
1 sbequ1 1939 . 2  |-  ( x  =  y  ->  ( ph  ->  [ y  /  x ] ph ) )
2 sbequ2 1657 . 2  |-  ( x  =  y  ->  ( [ y  /  x ] ph  ->  ph ) )
31, 2impbid 184 1  |-  ( x  =  y  ->  ( ph 
<->  [ y  /  x ] ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   [wsb 1655
This theorem is referenced by:  sbequ12r  1941  sbequ12a  1942  sbid  1943  ax16ALT  2104  ax16ALT2  2105  nfsb4t  2137  sbco  2140  sbco2  2143  sbcom  2146  sb8  2149  sb8e  2150  sbcom2  2171  sb6a  2174  sbal1  2184  mopick  2324  2mo  2340  2eu6  2347  clelab  2532  sbab  2534  cbvralf  2894  cbvralsv  2911  cbvrexsv  2912  cbvrab  2922  sbhypf  2969  mob2  3082  reu2  3090  reu6  3091  sbcralt  3201  sbcralg  3203  sbcrexg  3204  sbcreug  3205  cbvreucsf  3281  cbvrabcsf  3282  csbifg  3735  cbvopab1  4246  cbvopab1s  4248  csbopabg  4251  cbvmpt  4267  opelopabsb  4433  onminex  4754  tfis  4801  findes  4842  opeliunxp  4896  ralxpf  4986  cbviota  5390  csbiotag  5414  abrexex2g  5955  opabex3d  5956  opabex3  5957  abrexex2  5968  dfoprab4f  6372  cbvriota  6527  csbriotag  6529  uzind4s  10500  cbvmptf  24029  esumcvg  24437  pm13.193  27487  nfsb4twAUX7  29292  sbcoNEW7  29297  sbco2wAUX7  29300  sbcomwAUX7  29303  sb6aNEW7  29324  sbal1NEW7  29328  ax16ALTNEW7  29348  ax16ALT2OLD7  29439  nfsb4tOLD7  29441  nfsb4tw2AUXOLD7  29442  sbco2OLD7  29448  sbcomOLD7  29451  sbcom2OLD7  29457
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-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656
  Copyright terms: Public domain W3C validator