Theorem eqeq2 2774

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 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eqeq2d 2773	1 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754

This theorem is used by:  eqeq2i  2775  eqtr3  2784  clelab  2906  alexeqg  3608  pm13.183  3623  elab6g  3626  eqeu  3667  moeq3  3673  mo2icl  3675  mob2  3676  euind  3685  reu6i  3689  reu2eqd  3697  reuind  3714  sbc2or  3751  sbc5ALT  3771  csbiebg  3882  eqif  4527  sneq  4597  reusngf  4638  rexreusng  4643  reuprg0  4666  preq1b  4809  preq12bg  4816  preqsn  4825  disji2  5091  disjprg  5103  dtruALT  5357  opth  5456  euotd  5494  solin  5594  ideqg  5835  resieq  5987  cnveqb  6194  cnveq0  6195  reu3op  6294  reuop  6295  iota5  6520  funopg  6571  fneq2  6628  foeq3  6791  tz6.12f  6907  funbrfv  6930  fnbrfvb  6932  fvelimab  6954  elrnrexdm  7086  funsndifnop  7152  fconst5  7209  eufnfv  7232  f1veqaeq  7257  fpropnf1  7268  nf1const  7309  isosolem  7352  f1opr  7473  mpoeq123  7489  ovmpt4g  7564  ov3  7580  ovg  7582  caovcang  7619  caovcan  7622  tfisi  7859  tfindsg  7861  findsg  7898  f1oweALT  7973  seqomlem2  8444  oawordeu  8546  omopth  8654  ereq2  8709  qsdisj  8798  eroveu  8816  2dom  9041  fundmen  9042  xpf1o  9141  nneneq  9204  pwfir  9290  cantnflem1  9672  brttrcl  9696  ttrcltr  9699  ttrclss  9703  ttrclselem2  9709  updjud  9943  alephfp  10115  dfac5  10135  cardcf  10257  cfeq0  10262  sornom  10283  fpwwe2cbv  10643  fpwwe2lem3  10646  ltsosr  11107  map2psrpr  11123  axpre-lttri  11178  subval  11476  divval  11902  nn0ind-raph  12725  f1resfz0f1d  13852  fvf1tp  13854  uzrdgfni  14026  sqeqor  14284  nn0opth2  14340  hashrabsn1  14442  elprchashprn2  14464  hashbclem  14521  hashbc  14522  hash2prde  14539  hash2pwpr  14545  brfi1indALT  14579  wrdind  14795  wrd2ind  14796  reuccatpfxs1lem  14819  cshf1  14885  wrdl3s3  15039  relexpindlem  15140  sgnsub  15183  sqrtval  15328  sqrmo  15342  reusq0  15556  summolem2  15806  prodmolem2  16028  divides  16350  dvdstr  16390  odd2np1lem  16436  ndvdssub  16505  bitsinv1  16538  eucalglt  16681  hashgcdeq  16887  ramcl2lem  17107  ramcl  17127  cshwrepswhash1  17200  imasaddfnlem  17620  fnhomeqhomf  17785  initoeu2lem1  18109  cat1lem  18191  posi  18411  sgrp2nmndlem3  19043  degenmgm2nfun  19058  dfgrp2  19092  grpidinv  19128  dfgrp3lem  19167  orbsta  19446  symgfvne  19514  symgfix2  19549  odlem1  19668  gexlem1  19712  slwispgp  19744  sylow3lem6  19765  efgrelexlemb  19883  gsumval3lem2  20039  pgpfac1  20215  pgpfaclem2  20217  pgpfac  20219  ablfaclem1  20220  isdomn  20873  isdomn4  20883  domnlcanb  20887  domnrcanb  20889  obsip  21940  uvcval  22004  mvrval  22202  mhpval  22373  psdfval  22392  psdmvr  22403  coe1tmmul2  22508  coe1tmmul  22509  mat1comp  22668  mat1dimid  22702  scmateALT  22740  marrepval  22790  marepvval  22795  minmar1val  22876  gsummatr01  22887  t0sep  23555  t1sep2  23600  is2ndc  23677  kqt0lem  23968  isr0  23969  isufil2  24140  xmeteq0  24570  imasf1oxmet  24607  xrsxmet  25042  iccpnfcnv  25178  dyadmax  25832  dyadmbl  25834  dvfsumle  26255  dvfsumabs  26257  dvfsumlem1  26260  mdegle0  26309  fta1g  26402  ig1peu  26407  plyn0mulidp  26518  fta1  26545  aalioulem2  26576  taylthlem2  26617  efopn  26903  efrlim  27214  musum  27435  mpodvdsmulf1o  27438  dvdsmulf1o  27440  dchrsum2  27512  sumdchr2  27514  gausslemma2dlem0i  27608  addsqnreup  27687  2sqreulem1  27690  2sqreultblem  27692  2sqreunnlem1  27693  2sqreunnltblem  27695  2sqreulem3  27697  ltsres  27906  nosupprefixmo  27944  noinfprefixmo  27945  nosupcbv  27946  nosupno  27947  nosupfv  27950  noinfcbv  27961  noinfno  27962  noinffv  27965  elmade  28130  divsval  28462  noseqrdgfn  28579  bdayn0sf1o  28643  bdayfinbndlem2  28741  axtgcgrid  28812  axtgbtwnid  28815  tglowdim1i  28851  islmib  29179  prlngmo2  29321  axcontlem12  29440  upgredgpr  29607  ushgredgedg  29697  ushgredgedgloop  29699  rusgrpropnb  30051  rgrx0ndm  30061  uspgr2wlkeq  30113  wlkson  30122  upgrwlkdvdelem  30209  spthonepeq  30225  iswwlksnon  30329  wlklnwwlkln2lem  30358  wwlksnredwwlkn  30371  wwlksnextprop  30388  wwlksnwwlksnon  30391  elwwlks2ons3  30431  rusgrnumwwlklem  30449  clwlkclwwlklem2a4  30475  clwwlkn  30504  clwwlkext2edg  30534  hashecclwwlkn1  30555  umgrhashecclwwlk  30556  clwwlknon  30568  clwwlk0on0  30570  uhgr3cyclexlem  30669  1conngr  30682  frgr3vlem1  30761  3vfriswmgrlem  30765  frgrwopreglem3  30802  fusgreg2wsplem  30821  fusgreghash2wsp  30826  numclwlk1lem1  30857  numclwwlkovq  30862  numclwwlk2lem1  30864  frgrregord013  30883  friendshipgt3  30886  ex-opab  30920  isgrpoi  30987  grpoidinv2  31004  hvsubeq0  31557  hvaddcan  31559  hvsubadd  31566  normsub0  31625  omlsi  31893  pjoml  31925  nonbooli  32140  pj11  32203  lnopeq  32498  nmopun  32503  pjclem4a  32687  pj3lem1  32695  strlem4  32743  hstrlem4  32751  jplem1  32757  superpos  32843  ifeqeqx  33025  disji2f  33058  disjif2  33062  disjabrex  33063  disjabrexf  33064  disjxpin  33069  disjunsn  33075  ofpreima  33146  fgreu  33152  fcnvgreu  33153  gsumhashmul  33515  elrgspnlem2  33691  elrgspnlem3  33692  elrgspnlem4  33693  ismxidl  33873  mplasclco  34034  mplmulmvr  34057  psrmonmul2  34069  esplyfval  34081  esplyfval0  34082  esplyfv  34088  esplyfval3  34090  esplyfvaln  34092  xrge0iifcnv  34451  esumpr2  34585  eulerpartlemgvv  34895  eulerpartlemgh  34897  eulerpartlemgs2  34899  lpadmax  35201  lpadright  35203  bnj1321  35544  subfacp1lem3  35769  pconncn  35811  cnpconn  35817  txpconn  35819  connpconn  35822  cvmlift3lem2  35907  cvmlift3lem4  35909  cvmlift3  35915  snmlflim  35919  iota5f  36311  rankeq1o  36759  nn0prpw  36950  tr0elw  37111  tr0el  37112  dfttc4lem1  37155  elttcirr  37158  bj-csbsnlem  37654  bj-elgab  37691  bj-restsnss  37841  bj-restsnss2  37842  bj-imdirco  37950  wl-isseteq  38267  wl-ax12v2cl  38268  wl-dfcleq  38276  fin2so  38369  poimirlem2  38379  poimirlem18  38395  poimirlem21  38398  poimirlem25  38402  poimirlem26  38403  poimirlem27  38404  mblfinlem2  38415  mbfresfi  38423  cnambfre  38425  ftc1anclem8  38457  findcard4  38471  fdc  38503  istotbnd  38527  isexid2  38613  isgrpda  38713  ismaxidl  38798  mpobi123f  38918  mptbi12f  38922  disjressuc2  39167  qsdisjALTV  39455  parteq2  39634  lsatcmp  39884  lshpkrlem1  39991  trlval2  41044  cdlemg1cex  41469  cdlemm10N  41999  dicval  42057  lcmineqlem4  42906  grpods  43068  unitscyglem2  43070  unitscyglem3  43071  unitscyglem4  43072  exfinfldd  43077  nnn1suc  43155  resubval  43250  redivvald  43325  fsuppind  43444  unxpwdom3  43944  dgraalem  43994  dgraaub  43997  onsucf1lem  44118  frege104  44815  pm13.192  45242  2sbc6g  45247  2sbc5g  45248  pm14.122b  45255  equncomVD  45698  csbingVD  45714  csbsngVD  45723  csbxpgVD  45724  csbresgVD  45725  csbrngVD  45726  csbima12gALTVD  45727  csbunigVD  45728  csbfv12gALTVD  45729  relopabVD  45731  dvnprodlem1  46782  dvnprodlem2  46783  dvnprodlem3  46784  dvnprod  46785  fourierdlem42  46985  etransclem11  47081  etransclem12  47082  etransclem33  47103  nnfoctbdjlem  47291  hoimbl  47467  cfsetsnfsetf  47954  aiota0def  47992  euoreqb  48005  funressndmafv2rn  48119  funressnbrafv2  48140  dfatbrafv2b  48141  funbrafv2  48143  fnbrafv2b  48144  elsetpreimafvbi  48299  elsetpreimafveq  48305  imasetpreimafvbijlemfo  48313  fargshiftf1  48349  ichnreuop  48380  paireqne  48419  reupr  48430  isuspgrim0  48818  upgrimpths  48833  clnbgrgrim  48858  grimedg  48859  isubgr3stgrlem4  48893  isubgr3stgrlem7  48896  gpgedg2ov  48990  gpgedg2iv  48991  pgnbgreunbgrlem1  49037  pgnbgreunbgrlem2lem3  49040  pgnbgreunbgrlem4  49043  pgnbgreunbgr  49049  uspgrsprf1  49071  uspgrsprfo  49072  lidldomn1  49154  nn0sumshdiglem2  49560  mof0  49774  eufsnlem  49777  oppcmndclem  49951  isthincd2lem1  50359  termcbasmo  50417  termcarweu  50462  arweuthinc  50463  arweutermc  50464  setrec2lem2  50628