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  3614  pm13.183  3629  elab6g  3632  eqeu  3674  moeq3  3680  mo2icl  3682  mob2  3683  euind  3692  reu6i  3696  reu2eqd  3704  reuind  3721  sbc2or  3759  sbc5ALT  3779  csbiebg  3891  eqif  4526  sneq  4595  reusngf  4634  rexreusng  4639  reuprg0  4662  preq1b  4806  preq12bg  4813  preqsn  4822  disji2  5086  disjprg  5098  dtruALT  5338  opth  5431  euotd  5468  solin  5566  ideqg  5805  resieq  5950  cnveqb  6157  cnveq0  6158  reu3op  6253  reuop  6254  iota5  6482  funopg  6534  fneq2  6592  foeq3  6752  tz6.12f  6866  funbrfv  6891  fnbrfvb  6893  fvelimab  6915  elrnrexdm  7043  funsndifnop  7105  fconst5  7162  eufnfv  7185  f1veqaeq  7213  fpropnf1  7224  nf1const  7261  isosolem  7304  f1opr  7425  mpoeq123  7441  ovmpt4g  7516  ov3  7532  ovg  7534  caovcang  7570  caovcan  7573  tfisi  7815  tfindsg  7817  findsg  7853  f1oweALT  7930  seqomlem2  8396  oawordeu  8496  omopth  8603  ereq2  8656  qsdisj  8744  eroveu  8762  2dom  8978  fundmen  8979  xpf1o  9080  nneneq  9147  pwfir  9242  cantnflem1  9618  brttrcl  9642  ttrcltr  9645  ttrclss  9649  ttrclselem2  9655  updjud  9863  alephfp  10037  dfac5  10058  cardcf  10181  cfeq0  10185  sornom  10206  fpwwe2cbv  10559  fpwwe2lem3  10562  ltsosr  11023  map2psrpr  11039  axpre-lttri  11094  subval  11388  divval  11815  nn0ind-raph  12610  fvf1tp  13727  uzrdgfni  13899  sqeqor  14157  nn0opth2  14213  hashrabsn1  14315  elprchashprn2  14337  hashbclem  14393  hashbc  14394  hash2prde  14411  hash2pwpr  14417  brfi1indALT  14451  wrdind  14663  wrd2ind  14664  reuccatpfxs1lem  14687  cshf1  14751  wrdl3s3  14904  relexpindlem  15005  sqrtval  15179  sqrmo  15193  reusq0  15407  summolem2  15658  prodmolem2  15877  divides  16200  dvdstr  16240  odd2np1lem  16286  ndvdssub  16355  bitsinv1  16388  eucalglt  16531  hashgcdeq  16736  ramcl2lem  16956  ramcl  16976  cshwrepswhash1  17049  imasaddfnlem  17467  fnhomeqhomf  17628  initoeu2lem1  17952  cat1lem  18034  posi  18254  sgrp2nmndlem3  18828  dfgrp2  18870  grpidinv  18906  dfgrp3lem  18946  orbsta  19221  symgfvne  19287  symgfix2  19322  odlem1  19441  gexlem1  19485  slwispgp  19517  sylow3lem6  19538  efgrelexlemb  19656  gsumval3lem2  19812  pgpfac1  19988  pgpfaclem2  19990  pgpfac  19992  ablfaclem1  19993  isdomn  20590  isdomn4  20601  domnlcanb  20605  domnrcanb  20607  obsip  21606  uvcval  21670  mvrval  21867  mhpval  22002  psdfval  22021  psdmvr  22032  coe1tmmul2  22138  coe1tmmul  22139  mat1comp  22303  mat1dimid  22337  scmateALT  22375  marrepval  22425  marepvval  22430  minmar1val  22511  gsummatr01  22522  t0sep  23187  t1sep2  23232  is2ndc  23309  kqt0lem  23599  isr0  23600  isufil2  23771  xmeteq0  24202  imasf1oxmet  24239  xrsxmet  24674  iccpnfcnv  24818  dyadmax  25475  dyadmbl  25477  dvfsumle  25902  dvfsumleOLD  25903  dvfsumabs  25905  dvfsumlem1  25908  mdegle0  25958  fta1g  26051  ig1peu  26056  fta1  26192  aalioulem2  26217  taylthlem2  26258  efopn  26543  efrlim  26855  efrlimOLD  26856  musum  27077  mpodvdsmulf1o  27080  dvdsmulf1o  27082  dchrsum2  27155  sumdchr2  27157  gausslemma2dlem0i  27251  addsqnreup  27330  2sqreulem1  27333  2sqreultblem  27335  2sqreunnlem1  27336  2sqreunnltblem  27338  2sqreulem3  27340  sltres  27550  nosupprefixmo  27588  noinfprefixmo  27589  nosupcbv  27590  nosupno  27591  nosupfv  27594  noinfcbv  27605  noinfno  27606  noinffv  27609  elmade  27755  divsval  28068  noseqrdgfn  28176  bdayn0sf1o  28235  axtgcgrid  28366  axtgbtwnid  28369  tglowdim1i  28404  islmib  28690  axcontlem12  28878  upgredgpr  29045  ushgredgedg  29132  ushgredgedgloop  29134  rusgrpropnb  29487  rgrx0ndm  29497  uspgr2wlkeq  29549  wlkson  29558  upgrwlkdvdelem  29639  spthonepeq  29655  iswwlksnon  29756  wlklnwwlkln2lem  29785  wwlksnredwwlkn  29798  wwlksnextprop  29815  wwlksnwwlksnon  29818  elwwlks2ons3  29858  rusgrnumwwlklem  29873  clwlkclwwlklem2a4  29899  clwwlkn  29928  clwwlkext2edg  29958  hashecclwwlkn1  29979  umgrhashecclwwlk  29980  clwwlknon  29992  clwwlk0on0  29994  uhgr3cyclexlem  30083  1conngr  30096  frgr3vlem1  30175  3vfriswmgrlem  30179  frgrwopreglem3  30216  fusgreg2wsplem  30235  fusgreghash2wsp  30240  numclwlk1lem1  30271  numclwwlkovq  30276  numclwwlk2lem1  30278  frgrregord013  30297  friendshipgt3  30300  ex-opab  30334  isgrpoi  30400  grpoidinv2  30417  hvsubeq0  30970  hvaddcan  30972  hvsubadd  30979  normsub0  31038  omlsi  31306  pjoml  31338  nonbooli  31553  pj11  31616  lnopeq  31911  nmopun  31916  pjclem4a  32100  pj3lem1  32108  strlem4  32156  hstrlem4  32164  jplem1  32170  superpos  32256  ifeqeqx  32444  disji2f  32479  disjif2  32483  disjabrex  32484  disjabrexf  32485  disjxpin  32490  disjunsn  32496  ofpreima  32562  fgreu  32569  fcnvgreu  32570  sgnsub  32735  gsumhashmul  32974  elrgspnlem2  33167  elrgspnlem3  33168  elrgspnlem4  33169  domnlcanOLD  33203  ismxidl  33406  xrge0iifcnv  33896  esumpr2  34030  eulerpartlemgvv  34340  eulerpartlemgh  34342  eulerpartlemgs2  34344  plymulx0  34511  lpadmax  34646  lpadright  34648  bnj1321  34990  f1resfz0f1d  35074  subfacp1lem3  35142  pconncn  35184  cnpconn  35190  txpconn  35192  connpconn  35195  cvmlift3lem2  35280  cvmlift3lem4  35282  cvmlift3  35288  snmlflim  35292  iota5f  35684  rankeq1o  36132  nn0prpw  36284  bj-csbsnlem  36864  bj-elgab  36900  bj-restsnss  37044  bj-restsnss2  37045  bj-imdirco  37151  wl-isseteq  37466  wl-ax12v2cl  37467  fin2so  37574  poimirlem2  37589  poimirlem18  37605  poimirlem21  37608  poimirlem25  37612  poimirlem26  37613  poimirlem27  37614  mblfinlem2  37625  mbfresfi  37633  cnambfre  37635  ftc1anclem8  37667  fdc  37712  istotbnd  37736  isexid2  37822  isgrpda  37922  ismaxidl  38007  mpobi123f  38129  mptbi12f  38133  disjressuc2  38347  qsdisjALTV  38579  parteq2  38740  lsatcmp  38969  lshpkrlem1  39076  trlval2  40130  cdlemg1cex  40555  cdlemm10N  41085  dicval  41143  lcmineqlem4  41993  grpods  42155  unitscyglem2  42157  unitscyglem3  42158  unitscyglem4  42159  exfinfldd  42164  nnn1suc  42227  resubval  42328  redivvald  42403  fsuppind  42551  unxpwdom3  43057  dgraalem  43107  dgraaub  43110  onsucf1lem  43231  frege104  43929  pm13.192  44372  2sbc6g  44377  2sbc5g  44378  pm14.122b  44385  equncomVD  44830  csbingVD  44846  csbsngVD  44855  csbxpgVD  44856  csbresgVD  44857  csbrngVD  44858  csbima12gALTVD  44859  csbunigVD  44860  csbfv12gALTVD  44861  relopabVD  44863  dvnprodlem1  45917  dvnprodlem2  45918  dvnprodlem3  45919  dvnprod  45920  fourierdlem42  46120  etransclem11  46216  etransclem12  46217  etransclem33  46238  nnfoctbdjlem  46426  hoimbl  46602  cfsetsnfsetf  47032  aiota0def  47070  euoreqb  47083  funressndmafv2rn  47197  funressnbrafv2  47218  dfatbrafv2b  47219  funbrafv2  47221  fnbrafv2b  47222  elsetpreimafvbi  47365  elsetpreimafveq  47371  imasetpreimafvbijlemfo  47379  fargshiftf1  47415  ichnreuop  47446  paireqne  47485  reupr  47496  isuspgrim0  47867  upgrimpths  47882  clnbgrgrim  47907  grimedg  47908  isubgr3stgrlem4  47941  isubgr3stgrlem7  47944  gpgedg2ov  48030  gpgedg2iv  48031  pgnbgreunbgrlem1  48076  pgnbgreunbgrlem2lem3  48079  pgnbgreunbgrlem4  48082  pgnbgreunbgr  48088  uspgrsprf1  48108  uspgrsprfo  48109  lidldomn1  48192  nn0sumshdiglem2  48584  mof0  48799  eufsnlem  48802  oppcmndclem  48979  isthincd2lem1  49387  termcbasmo  49445  termcarweu  49490  arweuthinc  49491  arweutermc  49492  setrec2lem2  49656