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

Theorem eqeq2 2438
Description: Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
Assertion
Ref Expression
eqeq2  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )

Proof of Theorem eqeq2
StepHypRef Expression
1 id 23 . 2  |-  ( A  =  B  ->  A  =  B )
21eqeq2d 2437 1  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1438
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-cleq 2415
This theorem is referenced by:  eqeq2i  2441  eqeq12  2442  eleq1OLD  2497  neeq2OLD  2709  alexeqg  3201  alexeq  3202  pm13.183  3213  eqeu  3243  moeq3  3249  mo2icl  3251  mob2  3252  euind  3259  reu6i  3263  reu2eqd  3269  reuind  3276  sbc2or  3309  sbc5  3325  csbiebg  3419  eqif  3948  sneq  4007  preqr1  4172  prel12  4175  preq12bg  4177  prel12g  4178  disji2  4408  disjprg  4417  dtruALT  4651  dtruALT2  4663  opth  4693  euotd  4719  solin  4795  ideqg  5003  resieq  5132  cnveqb  5308  cnveq0  5309  ordequn  5540  iota5  5583  funopg  5631  fneq2  5681  foeq3  5806  tz6.12f  5897  funbrfv  5917  fnbrfvb  5919  fvelimab  5935  elrnrexdm  6039  fconst5  6135  eufnfv  6152  f1veqaeq  6174  isosolem  6251  mpt2eq123  6362  ovmpt4g  6431  ov3  6445  ovg  6447  caovcang  6482  caovcan  6485  tfisi  6697  tfindsg  6699  findsg  6732  f1oweALT  6789  seqomlem2  7174  oawordeu  7262  omopth  7365  ereq2  7377  qsdisj  7446  eroveu  7464  2dom  7647  fundmen  7648  xpf1o  7738  nneneq  7759  cantnflem1  8197  alephfp  8541  dfac5  8561  cardcf  8684  cfeq0  8688  sornom  8709  fpwwe2cbv  9057  fpwwe2lem3  9060  ltsosr  9520  map2psrpr  9536  axpre-lttri  9591  subval  9868  divval  10274  nn0ind-raph  11037  uzrdgfni  12173  sqeqor  12389  nn0opth2  12459  hashrabsn1  12554  elprchashprn2  12574  hashbclem  12614  hashbc  12615  hash2prde  12630  hash2pwpr  12633  brfi1indALT  12651  wrdind  12829  wrd2ind  12830  reuccats1lem  12832  relexpindlem  13120  sqrtval  13294  sqrmo  13309  summolem2  13775  prodmolem2  13982  divides  14300  dvdstr  14330  odd2np1lem  14357  ndvdssub  14381  bitsinv1  14409  eucalglt  14537  ramcl2lem  14955  ramcl2lemOLD  14956  ramcl  14980  cshwrepswhash1  15066  imasaddfnlem  15427  fnhomeqhomf  15589  initoeu2lem1  15902  posi  16188  sgrp2nmndlem3  16652  orbsta  16960  symgfvne  17022  symgfix2  17050  odlem1  17174  odlem1OLD  17177  gexlem1  17221  gexlem1OLD  17223  slwispgp  17256  sylow3lem6  17277  efgrelexlemb  17393  gsumval3lem2  17533  pgpfac1  17706  pgpfaclem2  17708  pgpfac  17710  ablfaclem1  17711  isdomn  18511  mvrval  18638  coe1tmmul2  18862  coe1tmmul  18863  obsip  19276  uvcval  19335  mat1comp  19457  mat1dimid  19491  scmateALT  19529  marrepval  19579  marepvval  19584  minmar1val  19665  gsummatr01  19676  t0sep  20332  t1sep2  20377  is2ndc  20453  kqt0lem  20743  isr0  20744  isufil2  20915  xmeteq0  21345  imasf1oxmet  21382  xrsxmet  21819  iccpnfcnv  21964  dyadmax  22548  dyadmbl  22550  dvfsumle  22965  dvfsumabs  22967  dvfsumlem1  22970  mdegle0  23018  fta1g  23110  ig1peu  23114  ig1peuOLD  23115  fta1  23253  aalioulem2  23281  efopn  23595  efrlim  23887  musum  24112  dvdsmulf1o  24115  dchrsum2  24188  sumdchr2  24190  axtgcgrid  24503  axtgbtwnid  24506  tglowdim1i  24537  islmib  24821  axcontlem12  24997  wlkon  25253  wlkntrllem3  25283  spthonepeq  25309  fargshiftf1  25357  constr3trllem2  25371  wlklniswwlkn2  25420  usg2wlkeq  25428  wwlknredwwlkn  25446  wwlkextprop  25464  clwwlkn  25487  clwlkisclwwlklem2a4  25504  clwwlkext2edg  25522  clwwnisshclwwn  25529  hashecclwwlkn1  25554  usghashecclwwlk  25555  clwlkfoclwwlk  25565  2wlkonot  25585  2spthonot  25586  el2wlkonot  25589  el2spthonot  25590  el2spthonot0  25591  rusgraprop2  25662  rusgrasn  25665  rusgranumwlklem1  25669  rusgranumwlklem2  25670  rusgranumwlklem3  25671  rusgranumwlkg  25678  clwlknclwlkdifs  25680  frgra3vlem1  25720  3vfriswmgralem  25724  usg2spot2nb  25785  usgreg2spot  25787  2spotmdisj  25788  usgreghash2spot  25789  numclwwlkdisj  25800  numclwwlkovf  25801  numclwwlkovg  25807  numclwlk1lem2f1  25814  numclwwlkovq  25819  numclwwlkovh  25821  numclwwlk5  25832  frgrareg  25837  frgraregord013  25838  friendshipgt3  25841  ex-opab  25874  isgrpoi  25918  grpoidinv2  25938  isgrp2d  25955  isgrpda  26017  isexid2  26045  ghgrpOLD  26088  hvsubeq0  26713  hvaddcan  26715  hvsubadd  26722  normsub0  26781  omlsi  27049  pjoml  27081  nonbooli  27296  pj11  27359  lnopeq  27654  nmopun  27659  pjclem4a  27843  pj3lem1  27851  strlem4  27899  hstrlem4  27907  jplem1  27913  superpos  27999  rmoeq  28115  ifeqeqx  28154  disji2f  28183  disjif2  28187  disjabrex  28188  disjabrexf  28189  disjxpin  28194  disjunsn  28200  ofpreima  28264  fgreu  28270  fcnvgreu  28271  xrge0iifcnv  28741  esumpr2  28890  eulerpartlemgvv  29211  eulerpartlemgh  29213  eulerpartlemgs2  29215  sgnsub  29417  plymulx0  29438  bnj1321  29838  subfacp1lem3  29907  pconcn  29949  cnpcon  29955  txpcon  29957  conpcon  29960  cvmlift3lem2  30045  cvmlift3lem4  30047  cvmlift3  30053  snmlflim  30057  ghomf1olem  30314  iota5f  30359  br1steqg  30417  br2ndeqg  30418  sltres  30552  nofulllem5  30594  rankeq1o  30937  nn0prpw  30978  bj-csbsnlem  31468  fin2so  31890  poimirlem2  31900  poimirlem18  31916  poimirlem21  31919  poimirlem25  31923  poimirlem26  31924  poimirlem27  31925  mblfinlem2  31936  mbfresfi  31945  cnambfre  31947  ftc1anclem8  31982  f1opr  32009  fdc  32032  istotbnd  32059  ismaxidl  32231  mpt2bi123f  32364  mptbi12f  32368  lsatcmp  32532  lshpkrlem1  32639  trlval2  33692  cdlemg1cex  34118  cdlemm10N  34649  dicval  34707  unxpwdom3  35917  dgraalem  35971  dgraalemOLD  35972  dgraaub  35977  dgraaubOLD  35978  hashgcdeq  36039  frege104  36465  pm13.192  36663  2sbc6g  36668  2sbc5g  36669  pm14.122b  36676  equncomVD  37170  csbingVD  37186  csbsngVD  37195  csbxpgVD  37196  csbresgVD  37197  csbrngVD  37198  csbima12gALTVD  37199  csbunigVD  37200  csbfv12gALTVD  37201  relopabVD  37203  disjinfi  37362  dvnprodlem1  37685  dvnprodlem2  37686  dvnprodlem3  37687  dvnprod  37688  fourierdlem42  37876  fourierdlem42OLD  37877  etransclem11  37974  etransclem12  37975  etransclem33  37996  nnfoctbdjlem  38116  reuccatpfxs1lem  38730  funsndifnop  38764  fundmge2nop  38768  usgredgedga  38969  lidldomn1  39263  nn0sumshdiglem2  39777
  Copyright terms: Public domain W3C validator