Theorem eqeq2 2633

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  eqeq2i  2634  eqeq12  2635  alexeqg  3332  clel5  3343  pm13.183  3344  eqeu  3377  moeq3  3383  mo2icl  3385  mob2  3386  euind  3393  reu6i  3397  reu2eqd  3403  reuind  3411  sbc2or  3444  sbc5  3460  csbiebg  3556  eqif  4126  sneq  4187  preq1b  4377  preqr1OLD  4380  prel12  4383  preq12bg  4386  prel12g  4387  preqsn  4393  disji2  4636  disjprg  4648  dtruALT  4899  dtruALT2  4911  opth  4945  euotd  4975  solin  5058  ideqg  5273  resieq  5407  cnveqb  5590  cnveq0  5591  iota5  5871  funopg  5922  fneq2  5980  foeq3  6113  tz6.12f  6212  funbrfv  6234  fnbrfvb  6236  fvelimab  6253  elrnrexdm  6363  funsndifnop  6416  fconst5  6471  eufnfv  6491  f1veqaeq  6514  fpropnf1  6524  isosolem  6597  mpt2eq123  6714  ovmpt4g  6783  ov3  6797  ovg  6799  caovcang  6835  caovcan  6838  tfisi  7058  tfindsg  7060  findsg  7093  f1oweALT  7152  seqomlem2  7546  oawordeu  7635  omopth  7738  ereq2  7750  qsdisj  7824  eroveu  7842  2dom  8029  fundmen  8030  xpf1o  8122  nneneq  8143  cantnflem1  8586  alephfp  8931  dfac5  8951  cardcf  9074  cfeq0  9078  sornom  9099  fpwwe2cbv  9452  fpwwe2lem3  9455  ltsosr  9915  map2psrpr  9931  axpre-lttri  9986  subval  10272  divval  10687  nn0ind-raph  11477  uzrdgfni  12757  sqeqor  12978  nn0opth2  13059  hashrabsn1  13163  elprchashprn2  13184  hashbclem  13236  hashbc  13237  hash2prde  13252  hash2pwpr  13258  brfi1indALT  13282  brfi1indALTOLD  13288  wrdind  13476  wrd2ind  13477  reuccats1lem  13479  cshf1  13556  wrdl3s3  13705  relexpindlem  13803  sqrtval  13977  sqrmo  13992  summolem2  14447  prodmolem2  14665  divides  14985  dvdstr  15018  odd2np1lem  15064  ndvdssub  15133  bitsinv1  15164  eucalglt  15298  hashgcdeq  15494  ramcl2lem  15713  ramcl  15733  cshwrepswhash1  15809  imasaddfnlem  16188  fnhomeqhomf  16351  initoeu2lem1  16664  posi  16950  sgrp2nmndlem3  17412  dfgrp2  17447  grpidinv  17475  dfgrp3lem  17513  orbsta  17746  symgfvne  17808  symgfix2  17836  odlem1  17954  gexlem1  17994  slwispgp  18026  sylow3lem6  18047  efgrelexlemb  18163  gsumval3lem2  18307  pgpfac1  18479  pgpfaclem2  18481  pgpfac  18483  ablfaclem1  18484  isdomn  19294  mvrval  19421  coe1tmmul2  19646  coe1tmmul  19647  obsip  20065  uvcval  20124  mat1comp  20246  mat1dimid  20280  scmateALT  20318  marrepval  20368  marepvval  20373  minmar1val  20454  gsummatr01  20465  t0sep  21128  t1sep2  21173  is2ndc  21249  kqt0lem  21539  isr0  21540  isufil2  21712  xmeteq0  22143  imasf1oxmet  22180  xrsxmet  22612  iccpnfcnv  22743  dyadmax  23366  dyadmbl  23368  dvfsumle  23784  dvfsumabs  23786  dvfsumlem1  23789  mdegle0  23837  fta1g  23927  ig1peu  23931  fta1  24063  aalioulem2  24088  efopn  24404  efrlim  24696  musum  24917  dvdsmulf1o  24920  dchrsum2  24993  sumdchr2  24995  gausslemma2dlem0i  25089  axtgcgrid  25362  axtgbtwnid  25365  tglowdim1i  25396  islmib  25679  axcontlem12  25855  upgredgpr  26037  ushgredgedg  26121  ushgredgedgloop  26123  rusgrpropnb  26479  rgrx0ndm  26489  uspgr2wlkeq  26542  wlkson  26552  upgrwlkdvdelem  26632  spthonepeq  26648  iswwlksnon  26740  wlklnwwlkln2lem  26768  wwlksnredwwlkn  26790  wwlksnextprop  26807  wwlksnwwlksnon  26810  wwlks2onv  26847  elwwlks2ons3  26848  rusgrnumwwlklem  26865  clwwlknclwwlkdifs  26873  clwwlksn  26881  clwlkclwwlklem2a4  26898  clwwlksext2edg  26923  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  clwlksfoclwwlk  26963  clwwlksndisj  26973  uhgr3cyclexlem  27041  1conngr  27054  frgr3vlem1  27137  3vfriswmgrlem  27141  frgrwopreglem3  27178  fusgreg2wsplem  27197  fusgreghash2wsp  27202  numclwwlkovf  27213  numclwwlkovg  27220  numclwlk1lem2f1  27227  numclwwlkovq  27232  numclwwlkovh  27234  numclwwlk2lem1  27235  frgrregord013  27253  friendshipgt3  27256  ex-opab  27289  isgrpoi  27352  grpoidinv2  27369  hvsubeq0  27925  hvaddcan  27927  hvsubadd  27934  normsub0  27993  omlsi  28263  pjoml  28295  nonbooli  28510  pj11  28573  lnopeq  28868  nmopun  28873  pjclem4a  29057  pj3lem1  29065  strlem4  29113  hstrlem4  29121  jplem1  29127  superpos  29213  rmoeqALT  29327  ifeqeqx  29361  disji2f  29390  disjif2  29394  disjabrex  29395  disjabrexf  29396  disjxpin  29401  disjunsn  29407  ofpreima  29465  fgreu  29471  fcnvgreu  29472  xrge0iifcnv  29979  esumpr2  30129  eulerpartlemgvv  30438  eulerpartlemgh  30440  eulerpartlemgs2  30442  sgnsub  30606  plymulx0  30624  bnj1321  31095  subfacp1lem3  31164  pconncn  31206  cnpconn  31212  txpconn  31214  connpconn  31217  cvmlift3lem2  31302  cvmlift3lem4  31304  cvmlift3  31310  snmlflim  31314  iota5f  31606  br1steqgOLD  31674  br2ndeqgOLD  31675  sltres  31815  noprefixmo  31848  nosupno  31849  nosupfv  31852  rankeq1o  32278  nn0prpw  32318  bj-csbsnlem  32898  bj-restsnss  33036  bj-restsnss2  33037  fin2so  33396  poimirlem2  33411  poimirlem18  33427  poimirlem21  33430  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  mblfinlem2  33447  mbfresfi  33456  cnambfre  33458  ftc1anclem8  33492  f1opr  33519  fdc  33541  istotbnd  33568  isexid2  33654  isgrpda  33754  ismaxidl  33839  mpt2bi123f  33971  mptbi12f  33975  lsatcmp  34290  lshpkrlem1  34397  trlval2  35450  cdlemg1cex  35876  cdlemm10N  36407  dicval  36465  unxpwdom3  37665  dgraalem  37715  dgraaub  37718  frege104  38261  pm13.192  38611  2sbc6g  38616  2sbc5g  38617  pm14.122b  38624  equncomVD  39104  csbingVD  39120  csbsngVD  39129  csbxpgVD  39130  csbresgVD  39131  csbrngVD  39132  csbima12gALTVD  39133  csbunigVD  39134  csbfv12gALTVD  39135  relopabVD  39137  dvnprodlem1  40161  dvnprodlem2  40162  dvnprodlem3  40163  dvnprod  40164  fourierdlem42  40366  etransclem11  40462  etransclem12  40463  etransclem33  40484  nnfoctbdjlem  40672  hoimbl  40845  fargshiftf1  41377  reuccatpfxs1lem  41433  uspgrsprf1  41755  uspgrsprfo  41756  lidldomn1  41921  nn0sumshdiglem2  42416  setrec2lem2  42441