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

Theorem sbequ12 1931
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 1930 . 2  |-  ( x  =  y  ->  ( ph  ->  [ y  /  x ] ph ) )
2 sbequ2 1655 . 2  |-  ( x  =  y  ->  ( [ y  /  x ] ph  ->  ph ) )
31, 2impbid 183 1  |-  ( x  =  y  ->  ( ph 
<->  [ y  /  x ] ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   [wsb 1653
This theorem is referenced by:  sbequ12r  1932  sbequ12a  1933  sbid  1934  ax16ALT  2060  ax16ALT2  2061  nfsb4t  2093  sbco  2096  sbco2  2099  sbcom  2102  sb8  2105  sb8e  2106  sbcom2  2127  sb6a  2129  sbal1  2139  mopick  2279  2mo  2295  2eu6  2302  clelab  2486  sbab  2488  cbvralf  2843  cbvralsv  2860  cbvrexsv  2861  cbvrab  2871  sbhypf  2918  mob2  3031  reu2  3039  reu6  3040  sbcralt  3149  sbcralg  3151  sbcrexg  3152  sbcreug  3153  cbvreucsf  3231  cbvrabcsf  3232  csbifg  3682  cbvopab1  4191  cbvopab1s  4193  csbopabg  4196  cbvmpt  4212  opelopabsb  4378  onminex  4701  tfis  4748  findes  4789  opeliunxp  4843  ralxpf  4933  cbviota  5327  csbiotag  5351  abrexex2g  5888  opabex3d  5889  opabex3  5890  abrexex2  5901  dfoprab4f  6305  cbvriota  6457  csbriotag  6459  uzind4s  10429  cbvmptf  23591  esumcvg  24062  itgaddnclem2  25767  pm13.193  27202  nfsb4twAUX7  28987  sbcoNEW7  28992  sbco2wAUX7  28995  sbcomwAUX7  28998  sb6aNEW7  29019  sbal1NEW7  29023  ax16ALTNEW7  29043  ax16ALT2OLD7  29134  nfsb4tOLD7  29136  nfsb4tw2AUXOLD7  29137  sbco2OLD7  29143  sbcomOLD7  29146  sbcom2OLD7  29152
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-11 1751
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1547  df-sb 1654
  Copyright terms: Public domain W3C validator