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 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

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

This theorem is referenced by:  eqeq2i  2747  eqeq12OLD  2753  eqtr3  2760  clelab  2884  alexeqg  3650  pm13.183  3665  elab6g  3668  eqeu  3714  moeq3  3720  mo2icl  3722  mob2  3723  euind  3732  reu6i  3736  reu2eqd  3744  reuind  3761  sbc2or  3799  sbc5ALT  3819  csbiebg  3940  eqif  4571  sneq  4640  reusngf  4678  rexreusng  4683  reuprg0  4706  preq1b  4850  preq12bg  4857  preqsn  4866  disji2  5131  disjprg  5143  dtruALT  5393  opth  5486  euotd  5522  solin  5622  ideqg  5864  resieq  6010  cnveqb  6217  cnveq0  6218  reu3op  6313  reuop  6314  iota5  6545  funopg  6601  fneq2  6660  foeq3  6818  tz6.12f  6932  funbrfv  6957  fnbrfvb  6959  fvelimab  6980  elrnrexdm  7108  funsndifnop  7170  fconst5  7225  eufnfv  7248  f1veqaeq  7276  fpropnf1  7286  nf1const  7323  isosolem  7366  f1opr  7488  mpoeq123  7504  ovmpt4g  7579  ov3  7595  ovg  7597  caovcang  7633  caovcan  7636  tfisi  7879  tfindsg  7881  findsg  7919  f1oweALT  7995  seqomlem2  8489  oawordeu  8591  omopth  8698  ereq2  8751  qsdisj  8832  eroveu  8850  2dom  9068  fundmen  9069  xpf1o  9177  nneneq  9243  nneneqOLD  9255  pwfir  9352  cantnflem1  9726  brttrcl  9750  ttrcltr  9753  ttrclss  9757  ttrclselem2  9763  updjud  9971  alephfp  10145  dfac5  10166  cardcf  10289  cfeq0  10293  sornom  10314  fpwwe2cbv  10667  fpwwe2lem3  10670  ltsosr  11131  map2psrpr  11147  axpre-lttri  11202  subval  11496  divval  11921  nn0ind-raph  12715  fvf1tp  13825  uzrdgfni  13995  sqeqor  14251  nn0opth2  14307  hashrabsn1  14409  elprchashprn2  14431  hashbclem  14487  hashbc  14488  hash2prde  14505  hash2pwpr  14511  brfi1indALT  14545  wrdind  14756  wrd2ind  14757  reuccatpfxs1lem  14780  cshf1  14844  wrdl3s3  14997  relexpindlem  15098  sqrtval  15272  sqrmo  15286  reusq0  15497  summolem2  15748  prodmolem2  15967  divides  16288  dvdstr  16327  odd2np1lem  16373  ndvdssub  16442  bitsinv1  16475  eucalglt  16618  hashgcdeq  16822  ramcl2lem  17042  ramcl  17062  cshwrepswhash1  17136  imasaddfnlem  17574  fnhomeqhomf  17735  initoeu2lem1  18067  cat1lem  18149  posi  18374  sgrp2nmndlem3  18950  dfgrp2  18992  grpidinv  19028  dfgrp3lem  19068  orbsta  19343  symgfvne  19412  symgfix2  19448  odlem1  19567  gexlem1  19611  slwispgp  19643  sylow3lem6  19664  efgrelexlemb  19782  gsumval3lem2  19938  pgpfac1  20114  pgpfaclem2  20116  pgpfac  20118  ablfaclem1  20119  isdomn  20721  isdomn4  20732  domnlcanb  20736  domnrcanb  20738  obsip  21758  uvcval  21822  mvrval  22019  mhpval  22160  psdfval  22179  coe1tmmul2  22294  coe1tmmul  22295  mat1comp  22461  mat1dimid  22495  scmateALT  22533  marrepval  22583  marepvval  22588  minmar1val  22669  gsummatr01  22680  t0sep  23347  t1sep2  23392  is2ndc  23469  kqt0lem  23759  isr0  23760  isufil2  23931  xmeteq0  24363  imasf1oxmet  24400  xrsxmet  24844  iccpnfcnv  24988  dyadmax  25646  dyadmbl  25648  dvfsumle  26074  dvfsumleOLD  26075  dvfsumabs  26077  dvfsumlem1  26080  mdegle0  26130  fta1g  26223  ig1peu  26228  fta1  26364  aalioulem2  26389  taylthlem2  26430  efopn  26714  efrlim  27026  efrlimOLD  27027  musum  27248  mpodvdsmulf1o  27251  dvdsmulf1o  27253  dchrsum2  27326  sumdchr2  27328  gausslemma2dlem0i  27422  addsqnreup  27501  2sqreulem1  27504  2sqreultblem  27506  2sqreunnlem1  27507  2sqreunnltblem  27509  2sqreulem3  27511  sltres  27721  nosupprefixmo  27759  noinfprefixmo  27760  nosupcbv  27761  nosupno  27762  nosupfv  27765  noinfcbv  27776  noinfno  27777  noinffv  27780  elmade  27920  divsval  28229  noseqrdgfn  28326  axtgcgrid  28485  axtgbtwnid  28488  tglowdim1i  28523  islmib  28809  axcontlem12  29004  upgredgpr  29173  ushgredgedg  29260  ushgredgedgloop  29262  rusgrpropnb  29615  rgrx0ndm  29625  uspgr2wlkeq  29678  wlkson  29688  upgrwlkdvdelem  29768  spthonepeq  29784  iswwlksnon  29882  wlklnwwlkln2lem  29911  wwlksnredwwlkn  29924  wwlksnextprop  29941  wwlksnwwlksnon  29944  elwwlks2ons3  29984  rusgrnumwwlklem  29999  clwlkclwwlklem2a4  30025  clwwlkn  30054  clwwlkext2edg  30084  hashecclwwlkn1  30105  umgrhashecclwwlk  30106  clwwlknon  30118  clwwlk0on0  30120  uhgr3cyclexlem  30209  1conngr  30222  frgr3vlem1  30301  3vfriswmgrlem  30305  frgrwopreglem3  30342  fusgreg2wsplem  30361  fusgreghash2wsp  30366  numclwlk1lem1  30397  numclwwlkovq  30402  numclwwlk2lem1  30404  frgrregord013  30423  friendshipgt3  30426  ex-opab  30460  isgrpoi  30526  grpoidinv2  30543  hvsubeq0  31096  hvaddcan  31098  hvsubadd  31105  normsub0  31164  omlsi  31432  pjoml  31464  nonbooli  31679  pj11  31742  lnopeq  32037  nmopun  32042  pjclem4a  32226  pj3lem1  32234  strlem4  32282  hstrlem4  32290  jplem1  32296  superpos  32382  ifeqeqx  32562  disji2f  32596  disjif2  32600  disjabrex  32601  disjabrexf  32602  disjxpin  32607  disjunsn  32613  ofpreima  32681  fgreu  32688  fcnvgreu  32689  gsumhashmul  33046  elrgspnlem2  33232  elrgspnlem3  33233  elrgspnlem4  33234  domnlcanOLD  33263  ismxidl  33469  xrge0iifcnv  33893  esumpr2  34047  eulerpartlemgvv  34357  eulerpartlemgh  34359  eulerpartlemgs2  34361  sgnsub  34525  plymulx0  34540  lpadmax  34675  lpadright  34677  bnj1321  35019  f1resfz0f1d  35097  subfacp1lem3  35166  pconncn  35208  cnpconn  35214  txpconn  35216  connpconn  35219  cvmlift3lem2  35304  cvmlift3lem4  35306  cvmlift3  35312  snmlflim  35316  iota5f  35703  rankeq1o  36152  nn0prpw  36305  bj-csbsnlem  36885  bj-elgab  36921  bj-restsnss  37065  bj-restsnss2  37066  bj-imdirco  37172  wl-isseteq  37485  wl-ax12v2cl  37486  fin2so  37593  poimirlem2  37608  poimirlem18  37624  poimirlem21  37627  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  mblfinlem2  37644  mbfresfi  37652  cnambfre  37654  ftc1anclem8  37686  fdc  37731  istotbnd  37755  isexid2  37841  isgrpda  37941  ismaxidl  38026  mpobi123f  38148  mptbi12f  38152  disjressuc2  38369  qsdisjALTV  38596  parteq2  38756  lsatcmp  38984  lshpkrlem1  39091  trlval2  40145  cdlemg1cex  40570  cdlemm10N  41100  dicval  41158  lcmineqlem4  42013  grpods  42175  unitscyglem2  42177  unitscyglem3  42178  unitscyglem4  42179  exfinfldd  42184  nnn1suc  42279  resubval  42373  fsuppind  42576  unxpwdom3  43083  dgraalem  43133  dgraaub  43136  onsucf1lem  43258  frege104  43956  pm13.192  44405  2sbc6g  44410  2sbc5g  44411  pm14.122b  44418  equncomVD  44865  csbingVD  44881  csbsngVD  44890  csbxpgVD  44891  csbresgVD  44892  csbrngVD  44893  csbima12gALTVD  44894  csbunigVD  44895  csbfv12gALTVD  44896  relopabVD  44898  dvnprodlem1  45901  dvnprodlem2  45902  dvnprodlem3  45903  dvnprod  45904  fourierdlem42  46104  etransclem11  46200  etransclem12  46201  etransclem33  46222  nnfoctbdjlem  46410  hoimbl  46586  cfsetsnfsetf  47007  aiota0def  47045  euoreqb  47058  funressndmafv2rn  47172  funressnbrafv2  47193  dfatbrafv2b  47194  funbrafv2  47196  fnbrafv2b  47197  elsetpreimafvbi  47315  elsetpreimafveq  47321  imasetpreimafvbijlemfo  47329  fargshiftf1  47365  ichnreuop  47396  paireqne  47435  reupr  47446  isuspgrim0  47809  clnbgrgrim  47839  grimedg  47840  isubgr3stgrlem4  47871  isubgr3stgrlem7  47874  uspgrsprf1  47990  uspgrsprfo  47991  lidldomn1  48074  nn0sumshdiglem2  48471  mof0  48667  eufsnlem  48670  isthincd2lem1  48826  setrec2lem2  48924