Theorem eqeq2 2743

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  eqeq2i  2744  eqtr3  2753  clelab  2876  alexeqg  3601  pm13.183  3616  elab6g  3619  eqeu  3660  moeq3  3666  mo2icl  3668  mob2  3669  euind  3678  reu6i  3682  reu2eqd  3690  reuind  3707  sbc2or  3745  sbc5ALT  3765  csbiebg  3877  eqif  4514  sneq  4583  reusngf  4624  rexreusng  4629  reuprg0  4652  preq1b  4795  preq12bg  4802  preqsn  4811  disji2  5073  disjprg  5085  dtruALT  5324  opth  5414  euotd  5451  solin  5549  ideqg  5790  resieq  5938  cnveqb  6143  cnveq0  6144  reu3op  6239  reuop  6240  iota5  6464  funopg  6515  fneq2  6573  foeq3  6733  tz6.12f  6847  funbrfv  6870  fnbrfvb  6872  fvelimab  6894  elrnrexdm  7022  funsndifnop  7084  fconst5  7140  eufnfv  7163  f1veqaeq  7190  fpropnf1  7201  nf1const  7238  isosolem  7281  f1opr  7402  mpoeq123  7418  ovmpt4g  7493  ov3  7509  ovg  7511  caovcang  7547  caovcan  7550  tfisi  7789  tfindsg  7791  findsg  7827  f1oweALT  7904  seqomlem2  8370  oawordeu  8470  omopth  8577  ereq2  8630  qsdisj  8718  eroveu  8736  2dom  8952  fundmen  8953  xpf1o  9052  nneneq  9115  pwfir  9201  cantnflem1  9579  brttrcl  9603  ttrcltr  9606  ttrclss  9610  ttrclselem2  9616  updjud  9827  alephfp  9999  dfac5  10020  cardcf  10143  cfeq0  10147  sornom  10168  fpwwe2cbv  10521  fpwwe2lem3  10524  ltsosr  10985  map2psrpr  11001  axpre-lttri  11056  subval  11351  divval  11778  nn0ind-raph  12573  fvf1tp  13693  uzrdgfni  13865  sqeqor  14123  nn0opth2  14179  hashrabsn1  14281  elprchashprn2  14303  hashbclem  14359  hashbc  14360  hash2prde  14377  hash2pwpr  14383  brfi1indALT  14417  wrdind  14629  wrd2ind  14630  reuccatpfxs1lem  14653  cshf1  14717  wrdl3s3  14869  relexpindlem  14970  sqrtval  15144  sqrmo  15158  reusq0  15372  summolem2  15623  prodmolem2  15842  divides  16165  dvdstr  16205  odd2np1lem  16251  ndvdssub  16320  bitsinv1  16353  eucalglt  16496  hashgcdeq  16701  ramcl2lem  16921  ramcl  16941  cshwrepswhash1  17014  imasaddfnlem  17432  fnhomeqhomf  17597  initoeu2lem1  17921  cat1lem  18003  posi  18223  sgrp2nmndlem3  18833  dfgrp2  18875  grpidinv  18911  dfgrp3lem  18951  orbsta  19225  symgfvne  19293  symgfix2  19328  odlem1  19447  gexlem1  19491  slwispgp  19523  sylow3lem6  19544  efgrelexlemb  19662  gsumval3lem2  19818  pgpfac1  19994  pgpfaclem2  19996  pgpfac  19998  ablfaclem1  19999  isdomn  20620  isdomn4  20631  domnlcanb  20635  domnrcanb  20637  obsip  21658  uvcval  21722  mvrval  21919  mhpval  22054  psdfval  22073  psdmvr  22084  coe1tmmul2  22190  coe1tmmul  22191  mat1comp  22355  mat1dimid  22389  scmateALT  22427  marrepval  22477  marepvval  22482  minmar1val  22563  gsummatr01  22574  t0sep  23239  t1sep2  23284  is2ndc  23361  kqt0lem  23651  isr0  23652  isufil2  23823  xmeteq0  24253  imasf1oxmet  24290  xrsxmet  24725  iccpnfcnv  24869  dyadmax  25526  dyadmbl  25528  dvfsumle  25953  dvfsumleOLD  25954  dvfsumabs  25956  dvfsumlem1  25959  mdegle0  26009  fta1g  26102  ig1peu  26107  fta1  26243  aalioulem2  26268  taylthlem2  26309  efopn  26594  efrlim  26906  efrlimOLD  26907  musum  27128  mpodvdsmulf1o  27131  dvdsmulf1o  27133  dchrsum2  27206  sumdchr2  27208  gausslemma2dlem0i  27302  addsqnreup  27381  2sqreulem1  27384  2sqreultblem  27386  2sqreunnlem1  27387  2sqreunnltblem  27389  2sqreulem3  27391  sltres  27601  nosupprefixmo  27639  noinfprefixmo  27640  nosupcbv  27641  nosupno  27642  nosupfv  27645  noinfcbv  27656  noinfno  27657  noinffv  27660  elmade  27812  divsval  28128  noseqrdgfn  28236  bdayn0sf1o  28295  axtgcgrid  28441  axtgbtwnid  28444  tglowdim1i  28479  islmib  28765  axcontlem12  28953  upgredgpr  29120  ushgredgedg  29207  ushgredgedgloop  29209  rusgrpropnb  29562  rgrx0ndm  29572  uspgr2wlkeq  29624  wlkson  29633  upgrwlkdvdelem  29714  spthonepeq  29730  iswwlksnon  29831  wlklnwwlkln2lem  29860  wwlksnredwwlkn  29873  wwlksnextprop  29890  wwlksnwwlksnon  29893  elwwlks2ons3  29933  rusgrnumwwlklem  29951  clwlkclwwlklem2a4  29977  clwwlkn  30006  clwwlkext2edg  30036  hashecclwwlkn1  30057  umgrhashecclwwlk  30058  clwwlknon  30070  clwwlk0on0  30072  uhgr3cyclexlem  30161  1conngr  30174  frgr3vlem1  30253  3vfriswmgrlem  30257  frgrwopreglem3  30294  fusgreg2wsplem  30313  fusgreghash2wsp  30318  numclwlk1lem1  30349  numclwwlkovq  30354  numclwwlk2lem1  30356  frgrregord013  30375  friendshipgt3  30378  ex-opab  30412  isgrpoi  30478  grpoidinv2  30495  hvsubeq0  31048  hvaddcan  31050  hvsubadd  31057  normsub0  31116  omlsi  31384  pjoml  31416  nonbooli  31631  pj11  31694  lnopeq  31989  nmopun  31994  pjclem4a  32178  pj3lem1  32186  strlem4  32234  hstrlem4  32242  jplem1  32248  superpos  32334  ifeqeqx  32522  disji2f  32557  disjif2  32561  disjabrex  32562  disjabrexf  32563  disjxpin  32568  disjunsn  32574  ofpreima  32647  fgreu  32654  fcnvgreu  32655  sgnsub  32820  gsumhashmul  33041  elrgspnlem2  33210  elrgspnlem3  33211  elrgspnlem4  33212  domnlcanOLD  33246  ismxidl  33427  esplyfval  33586  esplyfv  33591  xrge0iifcnv  33946  esumpr2  34080  eulerpartlemgvv  34389  eulerpartlemgh  34391  eulerpartlemgs2  34393  plymulx0  34560  lpadmax  34695  lpadright  34697  bnj1321  35039  f1resfz0f1d  35158  subfacp1lem3  35226  pconncn  35268  cnpconn  35274  txpconn  35276  connpconn  35279  cvmlift3lem2  35364  cvmlift3lem4  35366  cvmlift3  35372  snmlflim  35376  iota5f  35768  rankeq1o  36213  nn0prpw  36365  bj-csbsnlem  36945  bj-elgab  36981  bj-restsnss  37125  bj-restsnss2  37126  bj-imdirco  37232  wl-isseteq  37547  wl-ax12v2cl  37548  fin2so  37655  poimirlem2  37670  poimirlem18  37686  poimirlem21  37689  poimirlem25  37693  poimirlem26  37694  poimirlem27  37695  mblfinlem2  37706  mbfresfi  37714  cnambfre  37716  ftc1anclem8  37748  fdc  37793  istotbnd  37817  isexid2  37903  isgrpda  38003  ismaxidl  38088  mpobi123f  38210  mptbi12f  38214  disjressuc2  38428  qsdisjALTV  38660  parteq2  38821  lsatcmp  39050  lshpkrlem1  39157  trlval2  40210  cdlemg1cex  40635  cdlemm10N  41165  dicval  41223  lcmineqlem4  42073  grpods  42235  unitscyglem2  42237  unitscyglem3  42238  unitscyglem4  42239  exfinfldd  42244  nnn1suc  42307  resubval  42408  redivvald  42483  fsuppind  42631  unxpwdom3  43136  dgraalem  43186  dgraaub  43189  onsucf1lem  43310  frege104  44008  pm13.192  44451  2sbc6g  44456  2sbc5g  44457  pm14.122b  44464  equncomVD  44908  csbingVD  44924  csbsngVD  44933  csbxpgVD  44934  csbresgVD  44935  csbrngVD  44936  csbima12gALTVD  44937  csbunigVD  44938  csbfv12gALTVD  44939  relopabVD  44941  dvnprodlem1  45992  dvnprodlem2  45993  dvnprodlem3  45994  dvnprod  45995  fourierdlem42  46195  etransclem11  46291  etransclem12  46292  etransclem33  46313  nnfoctbdjlem  46501  hoimbl  46677  cfsetsnfsetf  47097  aiota0def  47135  euoreqb  47148  funressndmafv2rn  47262  funressnbrafv2  47283  dfatbrafv2b  47284  funbrafv2  47286  fnbrafv2b  47287  elsetpreimafvbi  47430  elsetpreimafveq  47436  imasetpreimafvbijlemfo  47444  fargshiftf1  47480  ichnreuop  47511  paireqne  47550  reupr  47561  isuspgrim0  47933  upgrimpths  47948  clnbgrgrim  47973  grimedg  47974  isubgr3stgrlem4  48008  isubgr3stgrlem7  48011  gpgedg2ov  48105  gpgedg2iv  48106  pgnbgreunbgrlem1  48152  pgnbgreunbgrlem2lem3  48155  pgnbgreunbgrlem4  48158  pgnbgreunbgr  48164  uspgrsprf1  48186  uspgrsprfo  48187  lidldomn1  48270  nn0sumshdiglem2  48662  mof0  48877  eufsnlem  48880  oppcmndclem  49057  isthincd2lem1  49465  termcbasmo  49523  termcarweu  49568  arweuthinc  49569  arweutermc  49570  setrec2lem2  49734