Theorem eqeq2 2749

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 2748	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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  eqeq2i  2750  eqeq12OLD  2756  eqtr3  2763  clelab  2887  alexeqg  3651  pm13.183  3666  elab6g  3669  eqeu  3712  moeq3  3718  mo2icl  3720  mob2  3721  euind  3730  reu6i  3734  reu2eqd  3742  reuind  3759  sbc2or  3797  sbc5ALT  3817  csbiebg  3931  eqif  4567  sneq  4636  reusngf  4674  rexreusng  4679  reuprg0  4702  preq1b  4846  preq12bg  4853  preqsn  4862  disji2  5127  disjprg  5139  dtruALT  5388  opth  5481  euotd  5518  solin  5619  ideqg  5862  resieq  6008  cnveqb  6216  cnveq0  6217  reu3op  6312  reuop  6313  iota5  6544  funopg  6600  fneq2  6660  foeq3  6818  tz6.12f  6932  funbrfv  6957  fnbrfvb  6959  fvelimab  6981  elrnrexdm  7109  funsndifnop  7171  fconst5  7226  eufnfv  7249  f1veqaeq  7277  fpropnf1  7287  nf1const  7324  isosolem  7367  f1opr  7489  mpoeq123  7505  ovmpt4g  7580  ov3  7596  ovg  7598  caovcang  7634  caovcan  7637  tfisi  7880  tfindsg  7882  findsg  7919  f1oweALT  7997  seqomlem2  8491  oawordeu  8593  omopth  8700  ereq2  8753  qsdisj  8834  eroveu  8852  2dom  9070  fundmen  9071  xpf1o  9179  nneneq  9246  nneneqOLD  9258  pwfir  9355  cantnflem1  9729  brttrcl  9753  ttrcltr  9756  ttrclss  9760  ttrclselem2  9766  updjud  9974  alephfp  10148  dfac5  10169  cardcf  10292  cfeq0  10296  sornom  10317  fpwwe2cbv  10670  fpwwe2lem3  10673  ltsosr  11134  map2psrpr  11150  axpre-lttri  11205  subval  11499  divval  11924  nn0ind-raph  12718  fvf1tp  13829  uzrdgfni  13999  sqeqor  14255  nn0opth2  14311  hashrabsn1  14413  elprchashprn2  14435  hashbclem  14491  hashbc  14492  hash2prde  14509  hash2pwpr  14515  brfi1indALT  14549  wrdind  14760  wrd2ind  14761  reuccatpfxs1lem  14784  cshf1  14848  wrdl3s3  15001  relexpindlem  15102  sqrtval  15276  sqrmo  15290  reusq0  15501  summolem2  15752  prodmolem2  15971  divides  16292  dvdstr  16331  odd2np1lem  16377  ndvdssub  16446  bitsinv1  16479  eucalglt  16622  hashgcdeq  16827  ramcl2lem  17047  ramcl  17067  cshwrepswhash1  17140  imasaddfnlem  17573  fnhomeqhomf  17734  initoeu2lem1  18059  cat1lem  18141  posi  18363  sgrp2nmndlem3  18938  dfgrp2  18980  grpidinv  19016  dfgrp3lem  19056  orbsta  19331  symgfvne  19398  symgfix2  19434  odlem1  19553  gexlem1  19597  slwispgp  19629  sylow3lem6  19650  efgrelexlemb  19768  gsumval3lem2  19924  pgpfac1  20100  pgpfaclem2  20102  pgpfac  20104  ablfaclem1  20105  isdomn  20705  isdomn4  20716  domnlcanb  20720  domnrcanb  20722  obsip  21741  uvcval  21805  mvrval  22002  mhpval  22143  psdfval  22162  psdmvr  22173  coe1tmmul2  22279  coe1tmmul  22280  mat1comp  22446  mat1dimid  22480  scmateALT  22518  marrepval  22568  marepvval  22573  minmar1val  22654  gsummatr01  22665  t0sep  23332  t1sep2  23377  is2ndc  23454  kqt0lem  23744  isr0  23745  isufil2  23916  xmeteq0  24348  imasf1oxmet  24385  xrsxmet  24831  iccpnfcnv  24975  dyadmax  25633  dyadmbl  25635  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  dvfsumlem1  26066  mdegle0  26116  fta1g  26209  ig1peu  26214  fta1  26350  aalioulem2  26375  taylthlem2  26416  efopn  26700  efrlim  27012  efrlimOLD  27013  musum  27234  mpodvdsmulf1o  27237  dvdsmulf1o  27239  dchrsum2  27312  sumdchr2  27314  gausslemma2dlem0i  27408  addsqnreup  27487  2sqreulem1  27490  2sqreultblem  27492  2sqreunnlem1  27493  2sqreunnltblem  27495  2sqreulem3  27497  sltres  27707  nosupprefixmo  27745  noinfprefixmo  27746  nosupcbv  27747  nosupno  27748  nosupfv  27751  noinfcbv  27762  noinfno  27763  noinffv  27766  elmade  27906  divsval  28215  noseqrdgfn  28312  axtgcgrid  28471  axtgbtwnid  28474  tglowdim1i  28509  islmib  28795  axcontlem12  28990  upgredgpr  29159  ushgredgedg  29246  ushgredgedgloop  29248  rusgrpropnb  29601  rgrx0ndm  29611  uspgr2wlkeq  29664  wlkson  29674  upgrwlkdvdelem  29756  spthonepeq  29772  iswwlksnon  29873  wlklnwwlkln2lem  29902  wwlksnredwwlkn  29915  wwlksnextprop  29932  wwlksnwwlksnon  29935  elwwlks2ons3  29975  rusgrnumwwlklem  29990  clwlkclwwlklem2a4  30016  clwwlkn  30045  clwwlkext2edg  30075  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  clwwlknon  30109  clwwlk0on0  30111  uhgr3cyclexlem  30200  1conngr  30213  frgr3vlem1  30292  3vfriswmgrlem  30296  frgrwopreglem3  30333  fusgreg2wsplem  30352  fusgreghash2wsp  30357  numclwlk1lem1  30388  numclwwlkovq  30393  numclwwlk2lem1  30395  frgrregord013  30414  friendshipgt3  30417  ex-opab  30451  isgrpoi  30517  grpoidinv2  30534  hvsubeq0  31087  hvaddcan  31089  hvsubadd  31096  normsub0  31155  omlsi  31423  pjoml  31455  nonbooli  31670  pj11  31733  lnopeq  32028  nmopun  32033  pjclem4a  32217  pj3lem1  32225  strlem4  32273  hstrlem4  32281  jplem1  32287  superpos  32373  ifeqeqx  32555  disji2f  32590  disjif2  32594  disjabrex  32595  disjabrexf  32596  disjxpin  32601  disjunsn  32607  ofpreima  32675  fgreu  32682  fcnvgreu  32683  gsumhashmul  33064  elrgspnlem2  33247  elrgspnlem3  33248  elrgspnlem4  33249  domnlcanOLD  33283  ismxidl  33490  xrge0iifcnv  33932  esumpr2  34068  eulerpartlemgvv  34378  eulerpartlemgh  34380  eulerpartlemgs2  34382  sgnsub  34547  plymulx0  34562  lpadmax  34697  lpadright  34699  bnj1321  35041  f1resfz0f1d  35119  subfacp1lem3  35187  pconncn  35229  cnpconn  35235  txpconn  35237  connpconn  35240  cvmlift3lem2  35325  cvmlift3lem4  35327  cvmlift3  35333  snmlflim  35337  iota5f  35724  rankeq1o  36172  nn0prpw  36324  bj-csbsnlem  36904  bj-elgab  36940  bj-restsnss  37084  bj-restsnss2  37085  bj-imdirco  37191  wl-isseteq  37506  wl-ax12v2cl  37507  fin2so  37614  poimirlem2  37629  poimirlem18  37645  poimirlem21  37648  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  mblfinlem2  37665  mbfresfi  37673  cnambfre  37675  ftc1anclem8  37707  fdc  37752  istotbnd  37776  isexid2  37862  isgrpda  37962  ismaxidl  38047  mpobi123f  38169  mptbi12f  38173  disjressuc2  38389  qsdisjALTV  38616  parteq2  38776  lsatcmp  39004  lshpkrlem1  39111  trlval2  40165  cdlemg1cex  40590  cdlemm10N  41120  dicval  41178  lcmineqlem4  42033  grpods  42195  unitscyglem2  42197  unitscyglem3  42198  unitscyglem4  42199  exfinfldd  42204  nnn1suc  42301  resubval  42397  fsuppind  42600  unxpwdom3  43107  dgraalem  43157  dgraaub  43160  onsucf1lem  43282  frege104  43980  pm13.192  44429  2sbc6g  44434  2sbc5g  44435  pm14.122b  44442  equncomVD  44888  csbingVD  44904  csbsngVD  44913  csbxpgVD  44914  csbresgVD  44915  csbrngVD  44916  csbima12gALTVD  44917  csbunigVD  44918  csbfv12gALTVD  44919  relopabVD  44921  dvnprodlem1  45961  dvnprodlem2  45962  dvnprodlem3  45963  dvnprod  45964  fourierdlem42  46164  etransclem11  46260  etransclem12  46261  etransclem33  46282  nnfoctbdjlem  46470  hoimbl  46646  cfsetsnfsetf  47070  aiota0def  47108  euoreqb  47121  funressndmafv2rn  47235  funressnbrafv2  47256  dfatbrafv2b  47257  funbrafv2  47259  fnbrafv2b  47260  elsetpreimafvbi  47378  elsetpreimafveq  47384  imasetpreimafvbijlemfo  47392  fargshiftf1  47428  ichnreuop  47459  paireqne  47498  reupr  47509  isuspgrim0  47872  clnbgrgrim  47902  grimedg  47903  isubgr3stgrlem4  47936  isubgr3stgrlem7  47939  uspgrsprf1  48063  uspgrsprfo  48064  lidldomn1  48147  nn0sumshdiglem2  48543  mof0  48747  eufsnlem  48750  oppcmndclem  48905  isthincd2lem1  49075  termcbasmo  49128  setrec2lem2  49213