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

Theorem eqeq2 2834
Description: Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
Assertion
Ref Expression
eqeq2 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))

Proof of Theorem eqeq2
StepHypRef Expression
1 id 22 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
21eqeq2d 2833 1 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2815
This theorem is referenced by:  eqeq2i  2835  eqeq12  2836  alexeqg  3619  pm13.183  3633  eqeu  3672  moeq3  3678  mo2icl  3680  mob2  3681  euind  3690  reu6i  3694  reu2eqd  3702  reuind  3719  sbc2or  3756  sbc5  3775  csbiebg  3887  eqif  4479  sneq  4549  reusngf  4586  rexreusng  4591  reuprg0  4612  preq1b  4750  preq12bg  4757  preqsn  4765  disji2  5024  disjprgw  5037  disjprg  5038  dtruALT  5266  dtruALT2  5313  opth  5345  euotd  5380  solin  5475  ideqg  5699  resieq  5842  cnveqb  6031  cnveq0  6032  reu3op  6121  reuop  6122  iota5  6317  funopg  6368  fneq2  6424  foeq3  6570  tz6.12f  6676  funbrfv  6698  fnbrfvb  6700  fvelimab  6719  elrnrexdm  6837  funsndifnop  6895  fconst5  6950  eufnfv  6974  f1veqaeq  6998  fpropnf1  7008  nf1const  7043  isosolem  7084  f1opr  7194  mpoeq123  7210  ovmpt4g  7281  ov3  7296  ovg  7298  caovcang  7334  caovcan  7337  tfisi  7558  tfindsg  7560  findsg  7595  f1oweALT  7659  seqomlem2  8074  oawordeu  8168  omopth  8272  ereq2  8284  qsdisj  8361  eroveu  8379  2dom  8569  fundmen  8570  xpf1o  8667  nneneq  8688  cantnflem1  9140  updjud  9351  alephfp  9523  dfac5  9543  cardcf  9663  cfeq0  9667  sornom  9688  fpwwe2cbv  10041  fpwwe2lem3  10044  ltsosr  10505  map2psrpr  10521  axpre-lttri  10576  subval  10866  divval  11289  nn0ind-raph  12070  uzrdgfni  13321  sqeqor  13574  nn0opth2  13628  hashrabsn1  13731  elprchashprn2  13753  hashbclem  13806  hashbc  13807  hash2prde  13824  hash2pwpr  13830  brfi1indALT  13854  wrdind  14075  wrd2ind  14076  reuccatpfxs1lem  14099  cshf1  14163  wrdl3s3  14317  relexpindlem  14413  sqrtval  14587  sqrmo  14602  reusq0  14813  summolem2  15064  prodmolem2  15280  divides  15600  dvdstr  15637  odd2np1lem  15680  ndvdssub  15749  bitsinv1  15780  eucalglt  15918  hashgcdeq  16115  ramcl2lem  16334  ramcl  16354  cshwrepswhash1  16427  imasaddfnlem  16792  fnhomeqhomf  16952  initoeu2lem1  17265  posi  17551  sgrp2nmndlem3  18081  dfgrp2  18119  grpidinv  18150  dfgrp3lem  18188  orbsta  18434  symgfvne  18500  symgfix2  18535  odlem1  18654  gexlem1  18695  slwispgp  18727  sylow3lem6  18748  efgrelexlemb  18867  gsumval3lem2  19017  pgpfac1  19193  pgpfaclem2  19195  pgpfac  19197  ablfaclem1  19198  isdomn  20058  obsip  20408  uvcval  20472  mvrval  20657  mhpval  20790  coe1tmmul2  20903  coe1tmmul  20904  mat1comp  21043  mat1dimid  21077  scmateALT  21115  marrepval  21165  marepvval  21170  minmar1val  21251  gsummatr01  21262  t0sep  21927  t1sep2  21972  is2ndc  22049  kqt0lem  22339  isr0  22340  isufil2  22511  xmeteq0  22943  imasf1oxmet  22980  xrsxmet  23412  iccpnfcnv  23547  dyadmax  24200  dyadmbl  24202  dvfsumle  24622  dvfsumabs  24624  dvfsumlem1  24627  mdegle0  24676  fta1g  24766  ig1peu  24770  fta1  24902  aalioulem2  24927  efopn  25247  efrlim  25553  musum  25774  dvdsmulf1o  25777  dchrsum2  25850  sumdchr2  25852  gausslemma2dlem0i  25946  addsqnreup  26025  2sqreulem1  26028  2sqreultblem  26030  2sqreunnlem1  26031  2sqreunnltblem  26033  2sqreulem3  26035  axtgcgrid  26255  axtgbtwnid  26258  tglowdim1i  26293  islmib  26579  axcontlem12  26767  upgredgpr  26933  ushgredgedg  27017  ushgredgedgloop  27019  rusgrpropnb  27371  rgrx0ndm  27381  uspgr2wlkeq  27433  wlkson  27444  upgrwlkdvdelem  27523  spthonepeq  27539  iswwlksnon  27637  wlklnwwlkln2lem  27666  wwlksnredwwlkn  27679  wwlksnextprop  27696  wwlksnwwlksnon  27699  elwwlks2ons3  27739  rusgrnumwwlklem  27754  clwlkclwwlklem2a4  27780  clwwlkn  27809  clwwlkext2edg  27839  hashecclwwlkn1  27860  umgrhashecclwwlk  27861  clwwlknon  27873  clwwlk0on0  27875  uhgr3cyclexlem  27964  1conngr  27977  frgr3vlem1  28056  3vfriswmgrlem  28060  frgrwopreglem3  28097  fusgreg2wsplem  28116  fusgreghash2wsp  28121  numclwlk1lem1  28152  numclwwlkovq  28157  numclwwlk2lem1  28159  frgrregord013  28178  friendshipgt3  28181  ex-opab  28215  isgrpoi  28279  grpoidinv2  28296  hvsubeq0  28849  hvaddcan  28851  hvsubadd  28858  normsub0  28917  omlsi  29185  pjoml  29217  nonbooli  29432  pj11  29495  lnopeq  29790  nmopun  29795  pjclem4a  29979  pj3lem1  29987  strlem4  30035  hstrlem4  30043  jplem1  30049  superpos  30135  ifeqeqx  30304  disji2f  30335  disjif2  30339  disjabrex  30340  disjabrexf  30341  disjxpin  30346  disjunsn  30352  ofpreima  30418  fgreu  30425  fcnvgreu  30426  ismxidl  31013  xrge0iifcnv  31250  esumpr2  31400  eulerpartlemgvv  31708  eulerpartlemgh  31710  eulerpartlemgs2  31712  sgnsub  31876  plymulx0  31891  lpadmax  32027  lpadright  32029  bnj1321  32373  f1resfz0f1d  32435  subfacp1lem3  32503  pconncn  32545  cnpconn  32551  txpconn  32553  connpconn  32556  cvmlift3lem2  32641  cvmlift3lem4  32643  cvmlift3  32649  snmlflim  32653  iota5f  33029  sltres  33243  noprefixmo  33276  nosupno  33277  nosupfv  33280  rankeq1o  33706  nn0prpw  33745  bj-csbsnlem  34305  bj-restsnss  34459  bj-restsnss2  34460  bj-imdirco  34566  fin2so  35003  poimirlem2  35018  poimirlem18  35034  poimirlem21  35037  poimirlem25  35041  poimirlem26  35042  poimirlem27  35043  mblfinlem2  35054  mbfresfi  35062  cnambfre  35064  ftc1anclem8  35096  fdc  35142  istotbnd  35166  isexid2  35252  isgrpda  35352  ismaxidl  35437  mpobi123f  35559  mptbi12f  35563  qsdisjALTV  35969  lsatcmp  36258  lshpkrlem1  36365  trlval2  37418  cdlemg1cex  37843  cdlemm10N  38373  dicval  38431  lcmineqlem4  39282  fsuppind  39404  nnn1suc  39412  resubval  39450  unxpwdom3  39970  dgraalem  40020  dgraaub  40023  frege104  40600  pm13.192  41049  2sbc6g  41054  2sbc5g  41055  pm14.122b  41062  equncomVD  41509  csbingVD  41525  csbsngVD  41534  csbxpgVD  41535  csbresgVD  41536  csbrngVD  41537  csbima12gALTVD  41538  csbunigVD  41539  csbfv12gALTVD  41540  relopabVD  41542  dvnprodlem1  42528  dvnprodlem2  42529  dvnprodlem3  42530  dvnprod  42531  fourierdlem42  42731  etransclem11  42827  etransclem12  42828  etransclem33  42849  nnfoctbdjlem  43034  hoimbl  43210  aiota0def  43591  euoreqb  43605  funressndmafv2rn  43719  funressnbrafv2  43740  dfatbrafv2b  43741  funbrafv2  43743  fnbrafv2b  43744  elsetpreimafvbi  43848  elsetpreimafveq  43854  imasetpreimafvbijlemfo  43862  fargshiftf1  43898  ichnreuop  43929  paireqne  43968  reupr  43979  uspgrsprf1  44315  uspgrsprfo  44316  lidldomn1  44485  nn0sumshdiglem2  44976  setrec2lem2  45164
  Copyright terms: Public domain W3C validator