Theorem eqeq2 2746

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 2745	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 2123  ax-ext 2706

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

This theorem is referenced by:  eqeq2i  2747  eqtr3  2756  clelab  2878  alexeqg  3603  pm13.183  3618  elab6g  3621  eqeu  3662  moeq3  3668  mo2icl  3670  mob2  3671  euind  3680  reu6i  3684  reu2eqd  3692  reuind  3709  sbc2or  3747  sbc5ALT  3767  csbiebg  3879  eqif  4519  sneq  4588  reusngf  4629  rexreusng  4634  reuprg0  4657  preq1b  4800  preq12bg  4807  preqsn  4816  disji2  5080  disjprg  5092  dtruALT  5331  opth  5422  euotd  5459  solin  5557  ideqg  5798  resieq  5947  cnveqb  6152  cnveq0  6153  reu3op  6248  reuop  6249  iota5  6473  funopg  6524  fneq2  6582  foeq3  6742  tz6.12f  6857  funbrfv  6880  fnbrfvb  6882  fvelimab  6904  elrnrexdm  7032  funsndifnop  7094  fconst5  7150  eufnfv  7173  f1veqaeq  7200  fpropnf1  7211  nf1const  7248  isosolem  7291  f1opr  7412  mpoeq123  7428  ovmpt4g  7503  ov3  7519  ovg  7521  caovcang  7557  caovcan  7560  tfisi  7799  tfindsg  7801  findsg  7837  f1oweALT  7914  seqomlem2  8380  oawordeu  8480  omopth  8588  ereq2  8641  qsdisj  8729  eroveu  8747  2dom  8965  fundmen  8966  xpf1o  9065  nneneq  9128  pwfir  9215  cantnflem1  9596  brttrcl  9620  ttrcltr  9623  ttrclss  9627  ttrclselem2  9633  updjud  9844  alephfp  10016  dfac5  10037  cardcf  10160  cfeq0  10164  sornom  10185  fpwwe2cbv  10539  fpwwe2lem3  10542  ltsosr  11003  map2psrpr  11019  axpre-lttri  11074  subval  11369  divval  11796  nn0ind-raph  12590  fvf1tp  13707  uzrdgfni  13879  sqeqor  14137  nn0opth2  14193  hashrabsn1  14295  elprchashprn2  14317  hashbclem  14373  hashbc  14374  hash2prde  14391  hash2pwpr  14397  brfi1indALT  14431  wrdind  14643  wrd2ind  14644  reuccatpfxs1lem  14667  cshf1  14731  wrdl3s3  14883  relexpindlem  14984  sqrtval  15158  sqrmo  15172  reusq0  15386  summolem2  15637  prodmolem2  15856  divides  16179  dvdstr  16219  odd2np1lem  16265  ndvdssub  16334  bitsinv1  16367  eucalglt  16510  hashgcdeq  16715  ramcl2lem  16935  ramcl  16955  cshwrepswhash1  17028  imasaddfnlem  17447  fnhomeqhomf  17612  initoeu2lem1  17936  cat1lem  18018  posi  18238  sgrp2nmndlem3  18848  dfgrp2  18890  grpidinv  18926  dfgrp3lem  18966  orbsta  19240  symgfvne  19308  symgfix2  19343  odlem1  19462  gexlem1  19506  slwispgp  19538  sylow3lem6  19559  efgrelexlemb  19677  gsumval3lem2  19833  pgpfac1  20009  pgpfaclem2  20011  pgpfac  20013  ablfaclem1  20014  isdomn  20636  isdomn4  20647  domnlcanb  20651  domnrcanb  20653  obsip  21674  uvcval  21738  mvrval  21935  mhpval  22080  psdfval  22099  psdmvr  22110  coe1tmmul2  22216  coe1tmmul  22217  mat1comp  22382  mat1dimid  22416  scmateALT  22454  marrepval  22504  marepvval  22509  minmar1val  22590  gsummatr01  22601  t0sep  23266  t1sep2  23311  is2ndc  23388  kqt0lem  23678  isr0  23679  isufil2  23850  xmeteq0  24280  imasf1oxmet  24317  xrsxmet  24752  iccpnfcnv  24896  dyadmax  25553  dyadmbl  25555  dvfsumle  25980  dvfsumleOLD  25981  dvfsumabs  25983  dvfsumlem1  25986  mdegle0  26036  fta1g  26129  ig1peu  26134  fta1  26270  aalioulem2  26295  taylthlem2  26336  efopn  26621  efrlim  26933  efrlimOLD  26934  musum  27155  mpodvdsmulf1o  27158  dvdsmulf1o  27160  dchrsum2  27233  sumdchr2  27235  gausslemma2dlem0i  27329  addsqnreup  27408  2sqreulem1  27411  2sqreultblem  27413  2sqreunnlem1  27414  2sqreunnltblem  27416  2sqreulem3  27418  sltres  27628  nosupprefixmo  27666  noinfprefixmo  27667  nosupcbv  27668  nosupno  27669  nosupfv  27672  noinfcbv  27683  noinfno  27684  noinffv  27687  elmade  27839  divsval  28158  noseqrdgfn  28267  bdayn0sf1o  28328  axtgcgrid  28484  axtgbtwnid  28487  tglowdim1i  28522  islmib  28808  axcontlem12  28997  upgredgpr  29164  ushgredgedg  29251  ushgredgedgloop  29253  rusgrpropnb  29606  rgrx0ndm  29616  uspgr2wlkeq  29668  wlkson  29677  upgrwlkdvdelem  29758  spthonepeq  29774  iswwlksnon  29875  wlklnwwlkln2lem  29904  wwlksnredwwlkn  29917  wwlksnextprop  29934  wwlksnwwlksnon  29937  elwwlks2ons3  29977  rusgrnumwwlklem  29995  clwlkclwwlklem2a4  30021  clwwlkn  30050  clwwlkext2edg  30080  hashecclwwlkn1  30101  umgrhashecclwwlk  30102  clwwlknon  30114  clwwlk0on0  30116  uhgr3cyclexlem  30205  1conngr  30218  frgr3vlem1  30297  3vfriswmgrlem  30301  frgrwopreglem3  30338  fusgreg2wsplem  30357  fusgreghash2wsp  30362  numclwlk1lem1  30393  numclwwlkovq  30398  numclwwlk2lem1  30400  frgrregord013  30419  friendshipgt3  30422  ex-opab  30456  isgrpoi  30522  grpoidinv2  30539  hvsubeq0  31092  hvaddcan  31094  hvsubadd  31101  normsub0  31160  omlsi  31428  pjoml  31460  nonbooli  31675  pj11  31738  lnopeq  32033  nmopun  32038  pjclem4a  32222  pj3lem1  32230  strlem4  32278  hstrlem4  32286  jplem1  32292  superpos  32378  ifeqeqx  32566  disji2f  32601  disjif2  32605  disjabrex  32606  disjabrexf  32607  disjxpin  32612  disjunsn  32618  ofpreima  32692  fgreu  32699  fcnvgreu  32700  sgnsub  32867  gsumhashmul  33099  elrgspnlem2  33274  elrgspnlem3  33275  elrgspnlem4  33276  domnlcanOLD  33311  ismxidl  33492  mplmulmvr  33653  esplyfval  33670  esplyfval0  33671  esplyfv  33677  esplyfval3  33679  xrge0iifcnv  34039  esumpr2  34173  eulerpartlemgvv  34482  eulerpartlemgh  34484  eulerpartlemgs2  34486  plymulx0  34653  lpadmax  34788  lpadright  34790  bnj1321  35132  f1resfz0f1d  35257  subfacp1lem3  35325  pconncn  35367  cnpconn  35373  txpconn  35375  connpconn  35378  cvmlift3lem2  35463  cvmlift3lem4  35465  cvmlift3  35471  snmlflim  35475  iota5f  35867  rankeq1o  36314  nn0prpw  36466  bj-csbsnlem  37047  bj-elgab  37083  bj-restsnss  37227  bj-restsnss2  37228  bj-imdirco  37334  wl-isseteq  37649  wl-ax12v2cl  37650  fin2so  37747  poimirlem2  37762  poimirlem18  37778  poimirlem21  37781  poimirlem25  37785  poimirlem26  37786  poimirlem27  37787  mblfinlem2  37798  mbfresfi  37806  cnambfre  37808  ftc1anclem8  37840  fdc  37885  istotbnd  37909  isexid2  37995  isgrpda  38095  ismaxidl  38180  mpobi123f  38302  mptbi12f  38306  disjressuc2  38535  qsdisjALTV  38811  parteq2  38973  lsatcmp  39202  lshpkrlem1  39309  trlval2  40362  cdlemg1cex  40787  cdlemm10N  41317  dicval  41375  lcmineqlem4  42225  grpods  42387  unitscyglem2  42389  unitscyglem3  42390  unitscyglem4  42391  exfinfldd  42396  nnn1suc  42463  resubval  42564  redivvald  42639  fsuppind  42775  unxpwdom3  43279  dgraalem  43329  dgraaub  43332  onsucf1lem  43453  frege104  44150  pm13.192  44593  2sbc6g  44598  2sbc5g  44599  pm14.122b  44606  equncomVD  45050  csbingVD  45066  csbsngVD  45075  csbxpgVD  45076  csbresgVD  45077  csbrngVD  45078  csbima12gALTVD  45079  csbunigVD  45080  csbfv12gALTVD  45081  relopabVD  45083  dvnprodlem1  46132  dvnprodlem2  46133  dvnprodlem3  46134  dvnprod  46135  fourierdlem42  46335  etransclem11  46431  etransclem12  46432  etransclem33  46453  nnfoctbdjlem  46641  hoimbl  46817  cfsetsnfsetf  47246  aiota0def  47284  euoreqb  47297  funressndmafv2rn  47411  funressnbrafv2  47432  dfatbrafv2b  47433  funbrafv2  47435  fnbrafv2b  47436  elsetpreimafvbi  47579  elsetpreimafveq  47585  imasetpreimafvbijlemfo  47593  fargshiftf1  47629  ichnreuop  47660  paireqne  47699  reupr  47710  isuspgrim0  48082  upgrimpths  48097  clnbgrgrim  48122  grimedg  48123  isubgr3stgrlem4  48157  isubgr3stgrlem7  48160  gpgedg2ov  48254  gpgedg2iv  48255  pgnbgreunbgrlem1  48301  pgnbgreunbgrlem2lem3  48304  pgnbgreunbgrlem4  48307  pgnbgreunbgr  48313  uspgrsprf1  48335  uspgrsprfo  48336  lidldomn1  48419  nn0sumshdiglem2  48810  mof0  49025  eufsnlem  49028  oppcmndclem  49204  isthincd2lem1  49612  termcbasmo  49670  termcarweu  49715  arweuthinc  49716  arweutermc  49717  setrec2lem2  49881