Theorem eqeq2 2742

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 2741	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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722

This theorem is referenced by:  eqeq2i  2743  eqtr3  2752  clelab  2874  alexeqg  3620  pm13.183  3635  elab6g  3638  eqeu  3680  moeq3  3686  mo2icl  3688  mob2  3689  euind  3698  reu6i  3702  reu2eqd  3710  reuind  3727  sbc2or  3765  sbc5ALT  3785  csbiebg  3897  eqif  4533  sneq  4602  reusngf  4641  rexreusng  4646  reuprg0  4669  preq1b  4813  preq12bg  4820  preqsn  4829  disji2  5094  disjprg  5106  dtruALT  5346  opth  5439  euotd  5476  solin  5576  ideqg  5818  resieq  5964  cnveqb  6172  cnveq0  6173  reu3op  6268  reuop  6269  iota5  6497  funopg  6553  fneq2  6613  foeq3  6773  tz6.12f  6887  funbrfv  6912  fnbrfvb  6914  fvelimab  6936  elrnrexdm  7064  funsndifnop  7126  fconst5  7183  eufnfv  7206  f1veqaeq  7234  fpropnf1  7245  nf1const  7282  isosolem  7325  f1opr  7448  mpoeq123  7464  ovmpt4g  7539  ov3  7555  ovg  7557  caovcang  7593  caovcan  7596  tfisi  7838  tfindsg  7840  findsg  7876  f1oweALT  7954  seqomlem2  8422  oawordeu  8522  omopth  8629  ereq2  8682  qsdisj  8770  eroveu  8788  2dom  9004  fundmen  9005  xpf1o  9109  nneneq  9176  pwfir  9273  cantnflem1  9649  brttrcl  9673  ttrcltr  9676  ttrclss  9680  ttrclselem2  9686  updjud  9894  alephfp  10068  dfac5  10089  cardcf  10212  cfeq0  10216  sornom  10237  fpwwe2cbv  10590  fpwwe2lem3  10593  ltsosr  11054  map2psrpr  11070  axpre-lttri  11125  subval  11419  divval  11846  nn0ind-raph  12641  fvf1tp  13758  uzrdgfni  13930  sqeqor  14188  nn0opth2  14244  hashrabsn1  14346  elprchashprn2  14368  hashbclem  14424  hashbc  14425  hash2prde  14442  hash2pwpr  14448  brfi1indALT  14482  wrdind  14694  wrd2ind  14695  reuccatpfxs1lem  14718  cshf1  14782  wrdl3s3  14935  relexpindlem  15036  sqrtval  15210  sqrmo  15224  reusq0  15438  summolem2  15689  prodmolem2  15908  divides  16231  dvdstr  16271  odd2np1lem  16317  ndvdssub  16386  bitsinv1  16419  eucalglt  16562  hashgcdeq  16767  ramcl2lem  16987  ramcl  17007  cshwrepswhash1  17080  imasaddfnlem  17498  fnhomeqhomf  17659  initoeu2lem1  17983  cat1lem  18065  posi  18285  sgrp2nmndlem3  18859  dfgrp2  18901  grpidinv  18937  dfgrp3lem  18977  orbsta  19252  symgfvne  19318  symgfix2  19353  odlem1  19472  gexlem1  19516  slwispgp  19548  sylow3lem6  19569  efgrelexlemb  19687  gsumval3lem2  19843  pgpfac1  20019  pgpfaclem2  20021  pgpfac  20023  ablfaclem1  20024  isdomn  20621  isdomn4  20632  domnlcanb  20636  domnrcanb  20638  obsip  21637  uvcval  21701  mvrval  21898  mhpval  22033  psdfval  22052  psdmvr  22063  coe1tmmul2  22169  coe1tmmul  22170  mat1comp  22334  mat1dimid  22368  scmateALT  22406  marrepval  22456  marepvval  22461  minmar1val  22542  gsummatr01  22553  t0sep  23218  t1sep2  23263  is2ndc  23340  kqt0lem  23630  isr0  23631  isufil2  23802  xmeteq0  24233  imasf1oxmet  24270  xrsxmet  24705  iccpnfcnv  24849  dyadmax  25506  dyadmbl  25508  dvfsumle  25933  dvfsumleOLD  25934  dvfsumabs  25936  dvfsumlem1  25939  mdegle0  25989  fta1g  26082  ig1peu  26087  fta1  26223  aalioulem2  26248  taylthlem2  26289  efopn  26574  efrlim  26886  efrlimOLD  26887  musum  27108  mpodvdsmulf1o  27111  dvdsmulf1o  27113  dchrsum2  27186  sumdchr2  27188  gausslemma2dlem0i  27282  addsqnreup  27361  2sqreulem1  27364  2sqreultblem  27366  2sqreunnlem1  27367  2sqreunnltblem  27369  2sqreulem3  27371  sltres  27581  nosupprefixmo  27619  noinfprefixmo  27620  nosupcbv  27621  nosupno  27622  nosupfv  27625  noinfcbv  27636  noinfno  27637  noinffv  27640  elmade  27786  divsval  28099  noseqrdgfn  28207  bdayn0sf1o  28266  axtgcgrid  28397  axtgbtwnid  28400  tglowdim1i  28435  islmib  28721  axcontlem12  28909  upgredgpr  29076  ushgredgedg  29163  ushgredgedgloop  29165  rusgrpropnb  29518  rgrx0ndm  29528  uspgr2wlkeq  29581  wlkson  29591  upgrwlkdvdelem  29673  spthonepeq  29689  iswwlksnon  29790  wlklnwwlkln2lem  29819  wwlksnredwwlkn  29832  wwlksnextprop  29849  wwlksnwwlksnon  29852  elwwlks2ons3  29892  rusgrnumwwlklem  29907  clwlkclwwlklem2a4  29933  clwwlkn  29962  clwwlkext2edg  29992  hashecclwwlkn1  30013  umgrhashecclwwlk  30014  clwwlknon  30026  clwwlk0on0  30028  uhgr3cyclexlem  30117  1conngr  30130  frgr3vlem1  30209  3vfriswmgrlem  30213  frgrwopreglem3  30250  fusgreg2wsplem  30269  fusgreghash2wsp  30274  numclwlk1lem1  30305  numclwwlkovq  30310  numclwwlk2lem1  30312  frgrregord013  30331  friendshipgt3  30334  ex-opab  30368  isgrpoi  30434  grpoidinv2  30451  hvsubeq0  31004  hvaddcan  31006  hvsubadd  31013  normsub0  31072  omlsi  31340  pjoml  31372  nonbooli  31587  pj11  31650  lnopeq  31945  nmopun  31950  pjclem4a  32134  pj3lem1  32142  strlem4  32190  hstrlem4  32198  jplem1  32204  superpos  32290  ifeqeqx  32478  disji2f  32513  disjif2  32517  disjabrex  32518  disjabrexf  32519  disjxpin  32524  disjunsn  32530  ofpreima  32596  fgreu  32603  fcnvgreu  32604  sgnsub  32769  gsumhashmul  33008  elrgspnlem2  33201  elrgspnlem3  33202  elrgspnlem4  33203  domnlcanOLD  33237  ismxidl  33440  xrge0iifcnv  33930  esumpr2  34064  eulerpartlemgvv  34374  eulerpartlemgh  34376  eulerpartlemgs2  34378  plymulx0  34545  lpadmax  34680  lpadright  34682  bnj1321  35024  f1resfz0f1d  35108  subfacp1lem3  35176  pconncn  35218  cnpconn  35224  txpconn  35226  connpconn  35229  cvmlift3lem2  35314  cvmlift3lem4  35316  cvmlift3  35322  snmlflim  35326  iota5f  35718  rankeq1o  36166  nn0prpw  36318  bj-csbsnlem  36898  bj-elgab  36934  bj-restsnss  37078  bj-restsnss2  37079  bj-imdirco  37185  wl-isseteq  37500  wl-ax12v2cl  37501  fin2so  37608  poimirlem2  37623  poimirlem18  37639  poimirlem21  37642  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  mblfinlem2  37659  mbfresfi  37667  cnambfre  37669  ftc1anclem8  37701  fdc  37746  istotbnd  37770  isexid2  37856  isgrpda  37956  ismaxidl  38041  mpobi123f  38163  mptbi12f  38167  disjressuc2  38381  qsdisjALTV  38613  parteq2  38774  lsatcmp  39003  lshpkrlem1  39110  trlval2  40164  cdlemg1cex  40589  cdlemm10N  41119  dicval  41177  lcmineqlem4  42027  grpods  42189  unitscyglem2  42191  unitscyglem3  42192  unitscyglem4  42193  exfinfldd  42198  nnn1suc  42261  resubval  42362  redivvald  42437  fsuppind  42585  unxpwdom3  43091  dgraalem  43141  dgraaub  43144  onsucf1lem  43265  frege104  43963  pm13.192  44406  2sbc6g  44411  2sbc5g  44412  pm14.122b  44419  equncomVD  44864  csbingVD  44880  csbsngVD  44889  csbxpgVD  44890  csbresgVD  44891  csbrngVD  44892  csbima12gALTVD  44893  csbunigVD  44894  csbfv12gALTVD  44895  relopabVD  44897  dvnprodlem1  45951  dvnprodlem2  45952  dvnprodlem3  45953  dvnprod  45954  fourierdlem42  46154  etransclem11  46250  etransclem12  46251  etransclem33  46272  nnfoctbdjlem  46460  hoimbl  46636  cfsetsnfsetf  47063  aiota0def  47101  euoreqb  47114  funressndmafv2rn  47228  funressnbrafv2  47249  dfatbrafv2b  47250  funbrafv2  47252  fnbrafv2b  47253  elsetpreimafvbi  47396  elsetpreimafveq  47402  imasetpreimafvbijlemfo  47410  fargshiftf1  47446  ichnreuop  47477  paireqne  47516  reupr  47527  isuspgrim0  47898  upgrimpths  47913  clnbgrgrim  47938  grimedg  47939  isubgr3stgrlem4  47972  isubgr3stgrlem7  47975  gpgedg2ov  48061  gpgedg2iv  48062  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem4  48113  pgnbgreunbgr  48119  uspgrsprf1  48139  uspgrsprfo  48140  lidldomn1  48223  nn0sumshdiglem2  48615  mof0  48830  eufsnlem  48833  oppcmndclem  49010  isthincd2lem1  49418  termcbasmo  49476  termcarweu  49521  arweuthinc  49522  arweutermc  49523  setrec2lem2  49687