Theorem eqeq2 2750

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

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eqeq2d 2749	1 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2730

This theorem is referenced by:  eqeq2i  2751  eqeq12OLD  2757  eqtr3  2764  clelab  2882  alexeqg  3600  pm13.183  3617  elab6g  3620  eqeu  3663  moeq3  3669  mo2icl  3671  mob2  3672  euind  3681  reu6i  3685  reu2eqd  3693  reuind  3710  sbc2or  3747  sbc5ALT  3767  csbiebg  3887  eqif  4526  sneq  4595  reusngf  4632  rexreusng  4639  reuprg0  4662  preq1b  4803  preq12bg  4810  preqsn  4818  disji2  5086  disjprgw  5099  disjprg  5100  dtruALT  5342  opth  5432  euotd  5468  solin  5568  ideqg  5804  resieq  5945  cnveqb  6145  cnveq0  6146  reu3op  6241  reuop  6242  iota5  6475  funopg  6531  fneq2  6590  foeq3  6750  tz6.12f  6864  funbrfv  6889  fnbrfvb  6891  fvelimab  6910  elrnrexdm  7034  funsndifnop  7092  fconst5  7150  eufnfv  7174  f1veqaeq  7199  fpropnf1  7209  nf1const  7245  isosolem  7287  f1opr  7406  mpoeq123  7422  ovmpt4g  7495  ov3  7510  ovg  7512  caovcang  7548  caovcan  7551  tfisi  7786  tfindsg  7788  findsg  7827  f1oweALT  7896  seqomlem2  8365  oawordeu  8470  omopth  8576  ereq2  8590  qsdisj  8667  eroveu  8685  2dom  8908  fundmen  8909  xpf1o  9017  pwfir  9054  nneneq  9087  nneneqOLD  9099  cantnflem1  9559  brttrcl  9583  ttrcltr  9586  ttrclss  9590  ttrclselem2  9596  updjud  9804  alephfp  9978  dfac5  9998  cardcf  10122  cfeq0  10126  sornom  10147  fpwwe2cbv  10500  fpwwe2lem3  10503  ltsosr  10964  map2psrpr  10980  axpre-lttri  11035  subval  11326  divval  11749  nn0ind-raph  12534  uzrdgfni  13792  sqeqor  14046  nn0opth2  14100  hashrabsn1  14202  elprchashprn2  14224  hashbclem  14277  hashbc  14278  hash2prde  14297  hash2pwpr  14303  brfi1indALT  14327  wrdind  14542  wrd2ind  14543  reuccatpfxs1lem  14566  cshf1  14630  wrdl3s3  14785  relexpindlem  14882  sqrtval  15056  sqrmo  15071  reusq0  15282  summolem2  15536  prodmolem2  15753  divides  16073  dvdstr  16111  odd2np1lem  16157  ndvdssub  16226  bitsinv1  16257  eucalglt  16396  hashgcdeq  16596  ramcl2lem  16816  ramcl  16836  cshwrepswhash1  16910  imasaddfnlem  17345  fnhomeqhomf  17506  initoeu2lem1  17835  cat1lem  17917  posi  18141  sgrp2nmndlem3  18670  dfgrp2  18710  grpidinv  18741  dfgrp3lem  18779  orbsta  19025  symgfvne  19094  symgfix2  19130  odlem1  19249  gexlem1  19290  slwispgp  19322  sylow3lem6  19343  efgrelexlemb  19461  gsumval3lem2  19612  pgpfac1  19788  pgpfaclem2  19790  pgpfac  19792  ablfaclem1  19793  isdomn  20687  obsip  21050  uvcval  21114  mvrval  21312  mhpval  21452  coe1tmmul2  21569  coe1tmmul  21570  mat1comp  21711  mat1dimid  21745  scmateALT  21783  marrepval  21833  marepvval  21838  minmar1val  21919  gsummatr01  21930  t0sep  22597  t1sep2  22642  is2ndc  22719  kqt0lem  23009  isr0  23010  isufil2  23181  xmeteq0  23613  imasf1oxmet  23650  xrsxmet  24094  iccpnfcnv  24229  dyadmax  24884  dyadmbl  24886  dvfsumle  25307  dvfsumabs  25309  dvfsumlem1  25312  mdegle0  25364  fta1g  25454  ig1peu  25458  fta1  25590  aalioulem2  25615  efopn  25935  efrlim  26241  musum  26462  dvdsmulf1o  26465  dchrsum2  26538  sumdchr2  26540  gausslemma2dlem0i  26634  addsqnreup  26713  2sqreulem1  26716  2sqreultblem  26718  2sqreunnlem1  26719  2sqreunnltblem  26721  2sqreulem3  26723  sltres  26932  nosupprefixmo  26970  noinfprefixmo  26971  nosupcbv  26972  nosupno  26973  nosupfv  26976  noinfcbv  26987  noinfno  26988  noinffv  26991  elmade  27118  axtgcgrid  27191  axtgbtwnid  27194  tglowdim1i  27229  islmib  27515  axcontlem12  27710  upgredgpr  27879  ushgredgedg  27963  ushgredgedgloop  27965  rusgrpropnb  28317  rgrx0ndm  28327  uspgr2wlkeq  28380  wlkson  28390  upgrwlkdvdelem  28470  spthonepeq  28486  iswwlksnon  28584  wlklnwwlkln2lem  28613  wwlksnredwwlkn  28626  wwlksnextprop  28643  wwlksnwwlksnon  28646  elwwlks2ons3  28686  rusgrnumwwlklem  28701  clwlkclwwlklem2a4  28727  clwwlkn  28756  clwwlkext2edg  28786  hashecclwwlkn1  28807  umgrhashecclwwlk  28808  clwwlknon  28820  clwwlk0on0  28822  uhgr3cyclexlem  28911  1conngr  28924  frgr3vlem1  29003  3vfriswmgrlem  29007  frgrwopreglem3  29044  fusgreg2wsplem  29063  fusgreghash2wsp  29068  numclwlk1lem1  29099  numclwwlkovq  29104  numclwwlk2lem1  29106  frgrregord013  29125  friendshipgt3  29128  ex-opab  29162  isgrpoi  29226  grpoidinv2  29243  hvsubeq0  29796  hvaddcan  29798  hvsubadd  29805  normsub0  29864  omlsi  30132  pjoml  30164  nonbooli  30379  pj11  30442  lnopeq  30737  nmopun  30742  pjclem4a  30926  pj3lem1  30934  strlem4  30982  hstrlem4  30990  jplem1  30996  superpos  31082  ifeqeqx  31249  disji2f  31280  disjif2  31284  disjabrex  31285  disjabrexf  31286  disjxpin  31291  disjunsn  31297  ofpreima  31366  fgreu  31373  fcnvgreu  31374  gsumhashmul  31680  ismxidl  32008  xrge0iifcnv  32275  esumpr2  32427  eulerpartlemgvv  32737  eulerpartlemgh  32739  eulerpartlemgs2  32741  sgnsub  32905  plymulx0  32920  lpadmax  33056  lpadright  33058  bnj1321  33400  f1resfz0f1d  33465  subfacp1lem3  33537  pconncn  33579  cnpconn  33585  txpconn  33587  connpconn  33590  cvmlift3lem2  33675  cvmlift3lem4  33677  cvmlift3  33683  snmlflim  33687  iota5f  34058  rankeq1o  34642  nn0prpw  34681  bj-csbsnlem  35256  bj-elgab  35295  bj-restsnss  35440  bj-restsnss2  35441  bj-imdirco  35547  fin2so  35951  poimirlem2  35966  poimirlem18  35982  poimirlem21  35985  poimirlem25  35989  poimirlem26  35990  poimirlem27  35991  mblfinlem2  36002  mbfresfi  36010  cnambfre  36012  ftc1anclem8  36044  fdc  36090  istotbnd  36114  isexid2  36200  isgrpda  36300  ismaxidl  36385  mpobi123f  36507  mptbi12f  36511  disjressuc2  36736  qsdisjALTV  36963  parteq2  37123  lsatcmp  37351  lshpkrlem1  37458  trlval2  38512  cdlemg1cex  38937  cdlemm10N  39467  dicval  39525  lcmineqlem4  40375  isdomn4  40510  fsuppind  40612  nnn1suc  40629  resubval  40683  unxpwdom3  41256  dgraalem  41306  dgraaub  41309  frege104  41970  pm13.192  42423  2sbc6g  42428  2sbc5g  42429  pm14.122b  42436  equncomVD  42883  csbingVD  42899  csbsngVD  42908  csbxpgVD  42909  csbresgVD  42910  csbrngVD  42911  csbima12gALTVD  42912  csbunigVD  42913  csbfv12gALTVD  42914  relopabVD  42916  dvnprodlem1  43897  dvnprodlem2  43898  dvnprodlem3  43899  dvnprod  43900  fourierdlem42  44100  etransclem11  44196  etransclem12  44197  etransclem33  44218  nnfoctbdjlem  44404  hoimbl  44580  cfsetsnfsetf  44992  aiota0def  45028  euoreqb  45041  funressndmafv2rn  45155  funressnbrafv2  45176  dfatbrafv2b  45177  funbrafv2  45179  fnbrafv2b  45180  elsetpreimafvbi  45283  elsetpreimafveq  45289  imasetpreimafvbijlemfo  45297  fargshiftf1  45333  ichnreuop  45364  paireqne  45403  reupr  45414  uspgrsprf1  45749  uspgrsprfo  45750  lidldomn1  45919  nn0sumshdiglem2  46408  mof0  46604  eufsnlem  46607  isthincd2lem1  46747  setrec2lem2  46839