Theorem eqeq2 2741

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 2740	1 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  eqeq2i  2742  eqtr3  2751  clelab  2873  alexeqg  3617  pm13.183  3632  elab6g  3635  eqeu  3677  moeq3  3683  mo2icl  3685  mob2  3686  euind  3695  reu6i  3699  reu2eqd  3707  reuind  3724  sbc2or  3762  sbc5ALT  3782  csbiebg  3894  eqif  4530  sneq  4599  reusngf  4638  rexreusng  4643  reuprg0  4666  preq1b  4810  preq12bg  4817  preqsn  4826  disji2  5091  disjprg  5103  dtruALT  5343  opth  5436  euotd  5473  solin  5573  ideqg  5815  resieq  5961  cnveqb  6169  cnveq0  6170  reu3op  6265  reuop  6266  iota5  6494  funopg  6550  fneq2  6610  foeq3  6770  tz6.12f  6884  funbrfv  6909  fnbrfvb  6911  fvelimab  6933  elrnrexdm  7061  funsndifnop  7123  fconst5  7180  eufnfv  7203  f1veqaeq  7231  fpropnf1  7242  nf1const  7279  isosolem  7322  f1opr  7445  mpoeq123  7461  ovmpt4g  7536  ov3  7552  ovg  7554  caovcang  7590  caovcan  7593  tfisi  7835  tfindsg  7837  findsg  7873  f1oweALT  7951  seqomlem2  8419  oawordeu  8519  omopth  8626  ereq2  8679  qsdisj  8767  eroveu  8785  2dom  9001  fundmen  9002  xpf1o  9103  nneneq  9170  pwfir  9266  cantnflem1  9642  brttrcl  9666  ttrcltr  9669  ttrclss  9673  ttrclselem2  9679  updjud  9887  alephfp  10061  dfac5  10082  cardcf  10205  cfeq0  10209  sornom  10230  fpwwe2cbv  10583  fpwwe2lem3  10586  ltsosr  11047  map2psrpr  11063  axpre-lttri  11118  subval  11412  divval  11839  nn0ind-raph  12634  fvf1tp  13751  uzrdgfni  13923  sqeqor  14181  nn0opth2  14237  hashrabsn1  14339  elprchashprn2  14361  hashbclem  14417  hashbc  14418  hash2prde  14435  hash2pwpr  14441  brfi1indALT  14475  wrdind  14687  wrd2ind  14688  reuccatpfxs1lem  14711  cshf1  14775  wrdl3s3  14928  relexpindlem  15029  sqrtval  15203  sqrmo  15217  reusq0  15431  summolem2  15682  prodmolem2  15901  divides  16224  dvdstr  16264  odd2np1lem  16310  ndvdssub  16379  bitsinv1  16412  eucalglt  16555  hashgcdeq  16760  ramcl2lem  16980  ramcl  17000  cshwrepswhash1  17073  imasaddfnlem  17491  fnhomeqhomf  17652  initoeu2lem1  17976  cat1lem  18058  posi  18278  sgrp2nmndlem3  18852  dfgrp2  18894  grpidinv  18930  dfgrp3lem  18970  orbsta  19245  symgfvne  19311  symgfix2  19346  odlem1  19465  gexlem1  19509  slwispgp  19541  sylow3lem6  19562  efgrelexlemb  19680  gsumval3lem2  19836  pgpfac1  20012  pgpfaclem2  20014  pgpfac  20016  ablfaclem1  20017  isdomn  20614  isdomn4  20625  domnlcanb  20629  domnrcanb  20631  obsip  21630  uvcval  21694  mvrval  21891  mhpval  22026  psdfval  22045  psdmvr  22056  coe1tmmul2  22162  coe1tmmul  22163  mat1comp  22327  mat1dimid  22361  scmateALT  22399  marrepval  22449  marepvval  22454  minmar1val  22535  gsummatr01  22546  t0sep  23211  t1sep2  23256  is2ndc  23333  kqt0lem  23623  isr0  23624  isufil2  23795  xmeteq0  24226  imasf1oxmet  24263  xrsxmet  24698  iccpnfcnv  24842  dyadmax  25499  dyadmbl  25501  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  dvfsumlem1  25932  mdegle0  25982  fta1g  26075  ig1peu  26080  fta1  26216  aalioulem2  26241  taylthlem2  26282  efopn  26567  efrlim  26879  efrlimOLD  26880  musum  27101  mpodvdsmulf1o  27104  dvdsmulf1o  27106  dchrsum2  27179  sumdchr2  27181  gausslemma2dlem0i  27275  addsqnreup  27354  2sqreulem1  27357  2sqreultblem  27359  2sqreunnlem1  27360  2sqreunnltblem  27362  2sqreulem3  27364  sltres  27574  nosupprefixmo  27612  noinfprefixmo  27613  nosupcbv  27614  nosupno  27615  nosupfv  27618  noinfcbv  27629  noinfno  27630  noinffv  27633  elmade  27779  divsval  28092  noseqrdgfn  28200  bdayn0sf1o  28259  axtgcgrid  28390  axtgbtwnid  28393  tglowdim1i  28428  islmib  28714  axcontlem12  28902  upgredgpr  29069  ushgredgedg  29156  ushgredgedgloop  29158  rusgrpropnb  29511  rgrx0ndm  29521  uspgr2wlkeq  29574  wlkson  29584  upgrwlkdvdelem  29666  spthonepeq  29682  iswwlksnon  29783  wlklnwwlkln2lem  29812  wwlksnredwwlkn  29825  wwlksnextprop  29842  wwlksnwwlksnon  29845  elwwlks2ons3  29885  rusgrnumwwlklem  29900  clwlkclwwlklem2a4  29926  clwwlkn  29955  clwwlkext2edg  29985  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  clwwlknon  30019  clwwlk0on0  30021  uhgr3cyclexlem  30110  1conngr  30123  frgr3vlem1  30202  3vfriswmgrlem  30206  frgrwopreglem3  30243  fusgreg2wsplem  30262  fusgreghash2wsp  30267  numclwlk1lem1  30298  numclwwlkovq  30303  numclwwlk2lem1  30305  frgrregord013  30324  friendshipgt3  30327  ex-opab  30361  isgrpoi  30427  grpoidinv2  30444  hvsubeq0  30997  hvaddcan  30999  hvsubadd  31006  normsub0  31065  omlsi  31333  pjoml  31365  nonbooli  31580  pj11  31643  lnopeq  31938  nmopun  31943  pjclem4a  32127  pj3lem1  32135  strlem4  32183  hstrlem4  32191  jplem1  32197  superpos  32283  ifeqeqx  32471  disji2f  32506  disjif2  32510  disjabrex  32511  disjabrexf  32512  disjxpin  32517  disjunsn  32523  ofpreima  32589  fgreu  32596  fcnvgreu  32597  sgnsub  32762  gsumhashmul  33001  elrgspnlem2  33194  elrgspnlem3  33195  elrgspnlem4  33196  domnlcanOLD  33230  ismxidl  33433  xrge0iifcnv  33923  esumpr2  34057  eulerpartlemgvv  34367  eulerpartlemgh  34369  eulerpartlemgs2  34371  plymulx0  34538  lpadmax  34673  lpadright  34675  bnj1321  35017  f1resfz0f1d  35101  subfacp1lem3  35169  pconncn  35211  cnpconn  35217  txpconn  35219  connpconn  35222  cvmlift3lem2  35307  cvmlift3lem4  35309  cvmlift3  35315  snmlflim  35319  iota5f  35711  rankeq1o  36159  nn0prpw  36311  bj-csbsnlem  36891  bj-elgab  36927  bj-restsnss  37071  bj-restsnss2  37072  bj-imdirco  37178  wl-isseteq  37493  wl-ax12v2cl  37494  fin2so  37601  poimirlem2  37616  poimirlem18  37632  poimirlem21  37635  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  mblfinlem2  37652  mbfresfi  37660  cnambfre  37662  ftc1anclem8  37694  fdc  37739  istotbnd  37763  isexid2  37849  isgrpda  37949  ismaxidl  38034  mpobi123f  38156  mptbi12f  38160  disjressuc2  38374  qsdisjALTV  38606  parteq2  38767  lsatcmp  38996  lshpkrlem1  39103  trlval2  40157  cdlemg1cex  40582  cdlemm10N  41112  dicval  41170  lcmineqlem4  42020  grpods  42182  unitscyglem2  42184  unitscyglem3  42185  unitscyglem4  42186  exfinfldd  42191  nnn1suc  42254  resubval  42355  redivvald  42430  fsuppind  42578  unxpwdom3  43084  dgraalem  43134  dgraaub  43137  onsucf1lem  43258  frege104  43956  pm13.192  44399  2sbc6g  44404  2sbc5g  44405  pm14.122b  44412  equncomVD  44857  csbingVD  44873  csbsngVD  44882  csbxpgVD  44883  csbresgVD  44884  csbrngVD  44885  csbima12gALTVD  44886  csbunigVD  44887  csbfv12gALTVD  44888  relopabVD  44890  dvnprodlem1  45944  dvnprodlem2  45945  dvnprodlem3  45946  dvnprod  45947  fourierdlem42  46147  etransclem11  46243  etransclem12  46244  etransclem33  46265  nnfoctbdjlem  46453  hoimbl  46629  cfsetsnfsetf  47059  aiota0def  47097  euoreqb  47110  funressndmafv2rn  47224  funressnbrafv2  47245  dfatbrafv2b  47246  funbrafv2  47248  fnbrafv2b  47249  elsetpreimafvbi  47392  elsetpreimafveq  47398  imasetpreimafvbijlemfo  47406  fargshiftf1  47442  ichnreuop  47473  paireqne  47512  reupr  47523  isuspgrim0  47894  upgrimpths  47909  clnbgrgrim  47934  grimedg  47935  isubgr3stgrlem4  47968  isubgr3stgrlem7  47971  gpgedg2ov  48057  gpgedg2iv  48058  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem2lem3  48106  pgnbgreunbgrlem4  48109  pgnbgreunbgr  48115  uspgrsprf1  48135  uspgrsprfo  48136  lidldomn1  48219  nn0sumshdiglem2  48611  mof0  48826  eufsnlem  48829  oppcmndclem  49006  isthincd2lem1  49414  termcbasmo  49472  termcarweu  49517  arweuthinc  49518  arweutermc  49519  setrec2lem2  49683