Theorem eqeq2 2751

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  eqeq2i  2752  eqtr3  2761  clelab  2883  alexeqg  3589  pm13.183  3604  elab6g  3607  eqeu  3647  moeq3  3653  mo2icl  3655  mob2  3656  euind  3665  reu6i  3669  reu2eqd  3677  reuind  3694  sbc2or  3732  sbc5ALT  3752  csbiebg  3863  eqif  4496  sneq  4565  reusngf  4606  rexreusng  4611  reuprg0  4634  preq1b  4777  preq12bg  4784  preqsn  4793  disji2  5056  disjprg  5068  dtruALT  5317  opth  5416  euotd  5454  solin  5553  ideqg  5793  resieq  5942  cnveqb  6147  cnveq0  6148  reu3op  6243  reuop  6244  iota5  6468  funopg  6519  fneq2  6577  foeq3  6737  tz6.12f  6852  funbrfv  6875  fnbrfvb  6877  fvelimab  6899  elrnrexdm  7030  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  8642  qsdisj  8731  eroveu  8749  2dom  8967  fundmen  8968  xpf1o  9067  nneneq  9130  pwfir  9217  cantnflem1  9601  brttrcl  9625  ttrcltr  9628  ttrclss  9632  ttrclselem2  9638  updjud  9849  alephfp  10021  dfac5  10042  cardcf  10165  cfeq0  10169  sornom  10190  fpwwe2cbv  10544  fpwwe2lem3  10547  ltsosr  11008  map2psrpr  11024  axpre-lttri  11079  subval  11375  divval  11802  nn0ind-raph  12620  fvf1tp  13739  uzrdgfni  13911  sqeqor  14169  nn0opth2  14225  hashrabsn1  14327  elprchashprn2  14349  hashbclem  14405  hashbc  14406  hash2prde  14423  hash2pwpr  14429  brfi1indALT  14463  wrdind  14675  wrd2ind  14676  reuccatpfxs1lem  14699  cshf1  14763  wrdl3s3  14915  relexpindlem  15016  sqrtval  15190  sqrmo  15204  reusq0  15418  summolem2  15669  prodmolem2  15891  divides  16214  dvdstr  16254  odd2np1lem  16300  ndvdssub  16369  bitsinv1  16402  eucalglt  16545  hashgcdeq  16751  ramcl2lem  16971  ramcl  16991  cshwrepswhash1  17064  imasaddfnlem  17483  fnhomeqhomf  17648  initoeu2lem1  17972  cat1lem  18054  posi  18274  sgrp2nmndlem3  18887  dfgrp2  18929  grpidinv  18965  dfgrp3lem  19005  orbsta  19279  symgfvne  19347  symgfix2  19382  odlem1  19501  gexlem1  19545  slwispgp  19577  sylow3lem6  19598  efgrelexlemb  19716  gsumval3lem2  19872  pgpfac1  20048  pgpfaclem2  20050  pgpfac  20052  ablfaclem1  20053  isdomn  20677  isdomn4  20688  domnlcanb  20692  domnrcanb  20694  obsip  21696  uvcval  21760  mvrval  21956  mhpval  22127  psdfval  22146  psdmvr  22157  coe1tmmul2  22262  coe1tmmul  22263  mat1comp  22423  mat1dimid  22457  scmateALT  22495  marrepval  22545  marepvval  22550  minmar1val  22631  gsummatr01  22642  t0sep  23307  t1sep2  23352  is2ndc  23429  kqt0lem  23719  isr0  23720  isufil2  23891  xmeteq0  24321  imasf1oxmet  24358  xrsxmet  24793  iccpnfcnv  24929  dyadmax  25583  dyadmbl  25585  dvfsumle  26006  dvfsumabs  26008  dvfsumlem1  26011  mdegle0  26060  fta1g  26153  ig1peu  26158  fta1  26292  aalioulem2  26317  taylthlem2  26357  efopn  26640  efrlim  26951  musum  27172  mpodvdsmulf1o  27175  dvdsmulf1o  27177  dchrsum2  27249  sumdchr2  27251  gausslemma2dlem0i  27345  addsqnreup  27424  2sqreulem1  27427  2sqreultblem  27429  2sqreunnlem1  27430  2sqreunnltblem  27432  2sqreulem3  27434  ltsres  27644  nosupprefixmo  27682  noinfprefixmo  27683  nosupcbv  27684  nosupno  27685  nosupfv  27688  noinfcbv  27699  noinfno  27700  noinffv  27703  elmade  27867  divsval  28199  noseqrdgfn  28316  bdayn0sf1o  28380  bdayfinbndlem2  28478  axtgcgrid  28549  axtgbtwnid  28552  tglowdim1i  28587  islmib  28873  axcontlem12  29062  upgredgpr  29229  ushgredgedg  29316  ushgredgedgloop  29318  rusgrpropnb  29670  rgrx0ndm  29680  uspgr2wlkeq  29732  wlkson  29741  upgrwlkdvdelem  29822  spthonepeq  29838  iswwlksnon  29939  wlklnwwlkln2lem  29968  wwlksnredwwlkn  29981  wwlksnextprop  29998  wwlksnwwlksnon  30001  elwwlks2ons3  30041  rusgrnumwwlklem  30059  clwlkclwwlklem2a4  30085  clwwlkn  30114  clwwlkext2edg  30144  hashecclwwlkn1  30165  umgrhashecclwwlk  30166  clwwlknon  30178  clwwlk0on0  30180  uhgr3cyclexlem  30269  1conngr  30282  frgr3vlem1  30361  3vfriswmgrlem  30365  frgrwopreglem3  30402  fusgreg2wsplem  30421  fusgreghash2wsp  30426  numclwlk1lem1  30457  numclwwlkovq  30462  numclwwlk2lem1  30464  frgrregord013  30483  friendshipgt3  30486  ex-opab  30520  isgrpoi  30587  grpoidinv2  30604  hvsubeq0  31157  hvaddcan  31159  hvsubadd  31166  normsub0  31225  omlsi  31493  pjoml  31525  nonbooli  31740  pj11  31803  lnopeq  32098  nmopun  32103  pjclem4a  32287  pj3lem1  32295  strlem4  32343  hstrlem4  32351  jplem1  32357  superpos  32443  ifeqeqx  32630  disji2f  32666  disjif2  32670  disjabrex  32671  disjabrexf  32672  disjxpin  32677  disjunsn  32683  ofpreima  32757  fgreu  32763  fcnvgreu  32764  sgnsub  32929  gsumhashmul  33148  elrgspnlem2  33324  elrgspnlem3  33325  elrgspnlem4  33326  domnlcanOLD  33361  ismxidl  33545  mplasclco  33700  mplmulmvr  33723  psrmonmul2  33735  esplyfval  33747  esplyfval0  33748  esplyfv  33754  esplyfval3  33756  esplyfvaln  33758  xrge0iifcnv  34117  esumpr2  34251  eulerpartlemgvv  34560  eulerpartlemgh  34562  eulerpartlemgs2  34564  plymulx0  34731  lpadmax  34866  lpadright  34868  bnj1321  35209  f1resfz0f1d  35342  subfacp1lem3  35410  pconncn  35452  cnpconn  35458  txpconn  35460  connpconn  35463  cvmlift3lem2  35548  cvmlift3lem4  35550  cvmlift3  35556  snmlflim  35560  iota5f  35952  rankeq1o  36399  nn0prpw  36551  tr0elw  36712  tr0el  36713  dfttc4lem1  36756  elttcirr  36759  bj-csbsnlem  37256  bj-elgab  37292  bj-restsnss  37441  bj-restsnss2  37442  bj-imdirco  37550  wl-isseteq  37867  wl-ax12v2cl  37868  wl-dfcleq  37876  fin2so  37974  poimirlem2  37989  poimirlem18  38005  poimirlem21  38008  poimirlem25  38012  poimirlem26  38013  poimirlem27  38014  mblfinlem2  38025  mbfresfi  38033  cnambfre  38035  ftc1anclem8  38067  fdc  38112  istotbnd  38136  isexid2  38222  isgrpda  38322  ismaxidl  38407  mpobi123f  38529  mptbi12f  38533  disjressuc2  38778  qsdisjALTV  39066  parteq2  39245  lsatcmp  39495  lshpkrlem1  39602  trlval2  40655  cdlemg1cex  41080  cdlemm10N  41610  dicval  41668  lcmineqlem4  42517  grpods  42679  unitscyglem2  42681  unitscyglem3  42682  unitscyglem4  42683  exfinfldd  42688  nnn1suc  42749  resubval  42844  redivvald  42919  fsuppind  43040  unxpwdom3  43540  dgraalem  43590  dgraaub  43593  onsucf1lem  43714  frege104  44411  pm13.192  44854  2sbc6g  44859  2sbc5g  44860  pm14.122b  44867  equncomVD  45311  csbingVD  45327  csbsngVD  45336  csbxpgVD  45337  csbresgVD  45338  csbrngVD  45339  csbima12gALTVD  45340  csbunigVD  45341  csbfv12gALTVD  45342  relopabVD  45344  dvnprodlem1  46389  dvnprodlem2  46390  dvnprodlem3  46391  dvnprod  46392  fourierdlem42  46592  etransclem11  46688  etransclem12  46689  etransclem33  46710  nnfoctbdjlem  46898  hoimbl  47074  cfsetsnfsetf  47521  aiota0def  47559  euoreqb  47572  funressndmafv2rn  47686  funressnbrafv2  47707  dfatbrafv2b  47708  funbrafv2  47710  fnbrafv2b  47711  elsetpreimafvbi  47866  elsetpreimafveq  47872  imasetpreimafvbijlemfo  47880  fargshiftf1  47916  ichnreuop  47947  paireqne  47986  reupr  47997  isuspgrim0  48385  upgrimpths  48400  clnbgrgrim  48425  grimedg  48426  isubgr3stgrlem4  48460  isubgr3stgrlem7  48463  gpgedg2ov  48557  gpgedg2iv  48558  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem2lem3  48607  pgnbgreunbgrlem4  48610  pgnbgreunbgr  48616  uspgrsprf1  48638  uspgrsprfo  48639  lidldomn1  48722  nn0sumshdiglem2  49113  mof0  49328  eufsnlem  49331  oppcmndclem  49507  isthincd2lem1  49915  termcbasmo  49973  termcarweu  50018  arweuthinc  50019  arweutermc  50020  setrec2lem2  50184