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

Theorem eqeq2 2472
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 22 . 2  |-  ( A  =  B  ->  A  =  B )
21eqeq2d 2471 1  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449
This theorem is referenced by:  eqeq2i  2475  eqeq12  2476  eleq1OLD  2531  neeq2OLD  2741  alexeqg  3228  alexeq  3229  pm13.183  3240  eqeu  3270  moeq3  3276  mo2icl  3278  mob2  3279  euind  3286  reu6i  3290  reu2eqd  3296  reuind  3303  sbc2or  3336  sbc5  3352  csbiebg  3453  eqif  3982  sneq  4042  preqr1  4206  prel12  4209  preq12bg  4211  prel12g  4212  disji2  4443  disjprg  4452  dtruALT  4688  dtruALT2  4700  opth  4730  euotd  4757  solin  4832  ordequn  4987  ideqg  5164  resieq  5294  cnveqb  5468  cnveq0  5469  iota5  5577  funopg  5626  fneq2  5676  foeq3  5799  tz6.12f  5890  funbrfv  5911  fnbrfvb  5913  fvelimab  5929  elrnrexdm  6036  fconst5  6130  eufnfv  6147  f1veqaeq  6169  isosolem  6244  mpt2eq123  6355  ovmpt4g  6424  ov3  6438  ovg  6440  caovcang  6475  caovcan  6478  tfisi  6692  tfindsg  6694  findsg  6726  f1oweALT  6783  seqomlem2  7134  oawordeu  7222  omopth  7325  ereq2  7337  qsdisj  7406  eroveu  7424  2dom  7607  fundmen  7608  xpf1o  7698  nneneq  7719  cantnflem1  8125  cantnflem1OLD  8148  alephfp  8506  dfac5  8526  cardcf  8649  cfeq0  8653  sornom  8674  fpwwe2cbv  9025  fpwwe2lem3  9028  ltsosr  9488  map2psrpr  9504  axpre-lttri  9559  subval  9830  divval  10230  nn0ind-raph  10985  uzrdgfni  12072  sqeqor  12285  nn0opth2  12355  hashrabsn1  12445  elprchashprn2  12465  hashbclem  12505  hashbc  12506  hash2prde  12520  hash2pwpr  12523  wrdind  12714  wrd2ind  12715  reuccats1lem  12717  sqrtval  13082  sqrmo  13097  summolem2  13550  prodmolem2  13754  divides  14000  dvdstr  14030  odd2np1lem  14057  ndvdssub  14077  bitsinv1  14104  eucalglt  14226  ramcl2lem  14539  ramcl  14559  cshwrepswhash1  14599  imasaddfnlem  14945  fnhomeqhomf  15107  initoeu2lem1  15420  posi  15706  sgrp2nmndlem3  16170  orbsta  16478  symgfvne  16540  symgfix2  16568  odlem1  16686  gexlem1  16726  slwispgp  16758  sylow3lem6  16779  efgrelexlemb  16895  gsumval3OLD  17035  gsumval3lem2  17037  pgpfac1  17258  pgpfaclem2  17260  pgpfac  17262  ablfaclem1  17263  isdomn  18070  mvrval  18204  coe1tmmul2  18444  coe1tmmul  18445  obsip  18879  uvcval  18943  mat1comp  19069  mat1dimid  19103  scmateALT  19141  marrepval  19191  marepvval  19196  minmar1val  19277  gsummatr01  19288  t0sep  19952  t1sep2  19997  is2ndc  20073  kqt0lem  20363  isr0  20364  isufil2  20535  xmeteq0  20967  imasf1oxmet  21004  xrsxmet  21440  iccpnfcnv  21570  dyadmax  22133  dyadmbl  22135  dvfsumle  22548  dvfsumabs  22550  dvfsumlem1  22553  mdegle0  22603  fta1g  22694  ig1peu  22698  fta1  22830  aalioulem2  22855  efopn  23165  efrlim  23425  musum  23593  dvdsmulf1o  23596  dchrsum2  23669  sumdchr2  23671  axtgcgrid  23986  axtgbtwnid  23989  tglowdim1i  24018  islmib  24279  axcontlem12  24405  wlkon  24660  wlkntrllem3  24690  spthonepeq  24716  fargshiftf1  24764  constr3trllem2  24778  wlklniswwlkn2  24827  usg2wlkeq  24835  wwlknredwwlkn  24853  wwlkextprop  24871  clwwlkn  24894  clwlkisclwwlklem2a4  24911  clwwlkext2edg  24929  clwwnisshclwwn  24936  hashecclwwlkn1  24961  usghashecclwwlk  24962  clwlkfoclwwlk  24972  2wlkonot  24992  2spthonot  24993  el2wlkonot  24996  el2spthonot  24997  el2spthonot0  24998  rusgraprop2  25069  rusgrasn  25072  rusgranumwlklem1  25076  rusgranumwlklem2  25077  rusgranumwlklem3  25078  rusgranumwlkg  25085  clwlknclwlkdifs  25087  frgra3vlem1  25127  3vfriswmgralem  25131  usg2spot2nb  25192  usgreg2spot  25194  2spotmdisj  25195  usgreghash2spot  25196  numclwwlkdisj  25207  numclwwlkovf  25208  numclwwlkovg  25214  numclwlk1lem2f1  25221  numclwwlkovq  25226  numclwwlkovh  25228  numclwwlk5  25239  frgrareg  25244  frgraregord013  25245  friendshipgt3  25248  ex-opab  25280  isgrpoi  25327  grpoidinv2  25347  isgrp2d  25364  isgrpda  25426  isexid2  25454  ghgrpOLD  25497  hvsubeq0  26112  hvaddcan  26114  hvsubadd  26121  normsub0  26180  omlsi  26449  pjoml  26481  nonbooli  26696  pj11  26759  lnopeq  27055  nmopun  27060  pjclem4a  27244  pj3lem1  27252  strlem4  27300  hstrlem4  27308  jplem1  27314  superpos  27400  rmoeq  27513  ifeqeqx  27554  disji2f  27577  disjif2  27581  disjabrex  27582  disjabrexf  27583  disjxpin  27587  disjunsn  27593  ofpreima  27661  fgreu  27667  fcnvgreu  27668  xrge0iifcnv  28076  esumpr2  28239  eulerpartlemgvv  28512  eulerpartlemgh  28514  eulerpartlemgs2  28516  sgnsub  28680  plymulx0  28701  subfacp1lem3  28823  pconcn  28866  cnpcon  28872  txpcon  28874  conpcon  28877  cvmlift3lem2  28962  cvmlift3lem4  28964  cvmlift3  28970  snmlflim  28974  ghomf1olem  29231  relexpindlem  29280  iota5f  29320  sltres  29641  nofulllem5  29683  rankeq1o  30033  fin2so  30245  mblfinlem2  30257  mbfresfi  30266  cnambfre  30268  ftc1anclem8  30302  nn0prpw  30346  f1opr  30420  fdc  30443  istotbnd  30470  ismaxidl  30642  mpt2bi123f  30776  mptbi12f  30780  unxpwdom3  31245  dgraalem  31298  dgraaub  31301  hashgcdeq  31362  pm13.192  31521  2sbc6g  31526  2sbc5g  31527  pm14.122b  31534  dvnprodlem1  31946  dvnprodlem2  31947  dvnprodlem3  31948  dvnprod  31949  fourierdlem42  32134  etransclem11  32231  etransclem12  32232  etransclem33  32253  reuccatpfxs1lem  32551  lidldomn1  32871  equncomVD  33811  csbingVD  33827  csbsngVD  33836  csbxpgVD  33837  csbresgVD  33838  csbrngVD  33839  csbima12gALTVD  33840  csbunigVD  33841  csbfv12gALTVD  33842  relopabVD  33844  bnj1321  34226  bj-csbsnlem  34613  lsatcmp  34871  lshpkrlem1  34978  trlval2  36031  cdlemg1cex  36457  cdlemm10N  36988  dicval  37046
  Copyright terms: Public domain W3C validator