Theorem eqeq2 2789

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-9 2059  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2771

This theorem is referenced by:  eqeq2i  2790  eqeq12  2791  alexeqg  3559  clel5OLD  3572  pm13.183  3573  pm13.183OLD  3574  eqeu  3611  moeq3  3617  mo2icl  3619  mob2  3620  euind  3627  reu6i  3631  reu2eqd  3639  reuind  3653  sbc2or  3690  sbc5  3706  csbiebg  3811  eqif  4390  sneq  4451  reusngf  4486  rexreusng  4491  reuprg0  4512  preq1b  4651  preq12bg  4658  preqsn  4666  disji2  4913  disjprg  4925  dtruALT  5141  dtruALT2  5192  opth  5225  euotd  5259  solin  5350  ideqg  5572  resieq  5709  cnveqb  5892  cnveq0  5893  reu3op  5981  reuop  5982  iota5  6172  funopg  6222  fneq2  6278  foeq3  6417  tz6.12f  6523  funbrfv  6546  fnbrfvb  6548  fvelimab  6566  elrnrexdm  6680  funsndifnop  6736  fconst5  6795  eufnfv  6817  f1veqaeq  6840  fpropnf1  6850  isosolem  6923  f1opr  7029  mpoeq123  7044  ovmpt4g  7113  ov3  7127  ovg  7129  caovcang  7165  caovcan  7168  tfisi  7389  tfindsg  7391  findsg  7424  f1oweALT  7485  seqomlem2  7890  oawordeu  7982  omopth  8085  ereq2  8097  qsdisj  8174  eroveu  8192  2dom  8379  fundmen  8380  xpf1o  8475  nneneq  8496  cantnflem1  8946  updjud  9157  alephfp  9328  dfac5  9348  cardcf  9472  cfeq0  9476  sornom  9497  fpwwe2cbv  9850  fpwwe2lem3  9853  ltsosr  10314  map2psrpr  10330  axpre-lttri  10385  subval  10677  divval  11101  nn0ind-raph  11895  uzrdgfni  13141  sqeqor  13393  nn0opth2  13447  hashrabsn1  13548  elprchashprn2  13570  hashbclem  13623  hashbc  13624  hash2prde  13639  hash2pwpr  13645  brfi1indALT  13669  wrdind  13915  wrdindOLD  13916  wrd2ind  13917  wrd2indOLD  13918  reuccats1lemOLD  13920  reuccatpfxs1lem  13955  cshf1  14034  wrdl3s3  14187  relexpindlem  14283  sqrtval  14457  sqrmo  14472  reusq0  14683  summolem2  14933  prodmolem2  15149  divides  15469  dvdstr  15506  odd2np1lem  15549  ndvdssub  15620  bitsinv1  15651  eucalglt  15785  hashgcdeq  15982  ramcl2lem  16201  ramcl  16221  cshwrepswhash1  16292  imasaddfnlem  16657  fnhomeqhomf  16819  initoeu2lem1  17132  posi  17418  sgrp2nmndlem3  17881  dfgrp2  17916  grpidinv  17946  dfgrp3lem  17984  orbsta  18214  symgfvne  18277  symgfix2  18305  odlem1  18425  gexlem1  18465  slwispgp  18497  sylow3lem6  18518  efgrelexlemb  18636  gsumval3lem2  18780  pgpfac1  18952  pgpfaclem2  18954  pgpfac  18956  ablfaclem1  18957  isdomn  19788  mvrval  19915  mhpval  20039  coe1tmmul2  20147  coe1tmmul  20148  obsip  20567  uvcval  20631  mat1comp  20753  mat1dimid  20787  scmateALT  20825  marrepval  20875  marepvval  20880  minmar1val  20961  gsummatr01  20972  t0sep  21636  t1sep2  21681  is2ndc  21758  kqt0lem  22048  isr0  22049  isufil2  22220  xmeteq0  22651  imasf1oxmet  22688  xrsxmet  23120  iccpnfcnv  23251  dyadmax  23902  dyadmbl  23904  dvfsumle  24321  dvfsumabs  24323  dvfsumlem1  24326  mdegle0  24374  fta1g  24464  ig1peu  24468  fta1  24600  aalioulem2  24625  efopn  24942  efrlim  25249  musum  25470  dvdsmulf1o  25473  dchrsum2  25546  sumdchr2  25548  gausslemma2dlem0i  25642  addsqnreup  25721  2sqreulem1  25724  2sqreultblem  25726  2sqreunnlem1  25727  2sqreunnltblem  25729  2sqreulem3  25731  axtgcgrid  25951  axtgbtwnid  25954  tglowdim1i  25989  islmib  26275  axcontlem12  26464  upgredgpr  26630  ushgredgedg  26714  ushgredgedgloop  26716  rusgrpropnb  27068  rgrx0ndm  27078  uspgr2wlkeq  27130  wlkson  27140  upgrwlkdvdelem  27225  spthonepeq  27241  iswwlksnon  27339  wlklnwwlkln2lem  27369  wwlksnredwwlkn  27384  wwlksnredwwlknOLD  27385  wwlksnextprop  27415  wwlksnextpropOLD  27416  wwlksnwwlksnon  27421  elwwlks2ons3  27461  rusgrnumwwlklem  27476  clwlkclwwlklem2a4  27503  clwwlkn  27541  clwwlkext2edg  27579  hashecclwwlkn1  27601  umgrhashecclwwlk  27602  clwwlknon  27618  clwwlk0on0  27620  uhgr3cyclexlem  27710  1conngr  27723  frgr3vlem1  27807  3vfriswmgrlem  27811  frgrwopreglem3  27848  fusgreg2wsplem  27867  fusgreghash2wsp  27872  numclwlk1lem1  27922  numclwwlkovq  27927  numclwwlk2lem1  27929  frgrregord013  27952  friendshipgt3  27955  ex-opab  27989  isgrpoi  28052  grpoidinv2  28069  hvsubeq0  28624  hvaddcan  28626  hvsubadd  28633  normsub0  28692  omlsi  28962  pjoml  28994  nonbooli  29209  pj11  29272  lnopeq  29567  nmopun  29572  pjclem4a  29756  pj3lem1  29764  strlem4  29812  hstrlem4  29820  jplem1  29826  superpos  29912  ifeqeqx  30065  disji2f  30093  disjif2  30097  disjabrex  30098  disjabrexf  30099  disjxpin  30104  disjunsn  30110  ofpreima  30172  fgreu  30179  fcnvgreu  30180  xrge0iifcnv  30826  esumpr2  30976  eulerpartlemgvv  31285  eulerpartlemgh  31287  eulerpartlemgs2  31289  sgnsub  31454  plymulx0  31469  lpadmax  31607  lpadright  31609  bnj1321  31950  subfacp1lem3  32020  pconncn  32062  cnpconn  32068  txpconn  32070  connpconn  32073  cvmlift3lem2  32158  cvmlift3lem4  32160  cvmlift3  32166  snmlflim  32170  iota5f  32481  sltres  32696  noprefixmo  32729  nosupno  32730  nosupfv  32733  rankeq1o  33159  nn0prpw  33198  bj-csbsnlem  33718  bj-restsnss  33890  bj-restsnss2  33891  fin2so  34326  poimirlem2  34341  poimirlem18  34357  poimirlem21  34360  poimirlem25  34364  poimirlem26  34365  poimirlem27  34366  mblfinlem2  34377  mbfresfi  34385  cnambfre  34387  ftc1anclem8  34421  fdc  34468  istotbnd  34495  isexid2  34581  isgrpda  34681  ismaxidl  34766  mpobi123f  34890  mptbi12f  34894  qsdisjALTV  35301  lsatcmp  35590  lshpkrlem1  35697  trlval2  36750  cdlemg1cex  37175  cdlemm10N  37705  dicval  37763  nnn1suc  38600  resubval  38635  unxpwdom3  39097  dgraalem  39147  dgraaub  39150  frege104  39682  pm13.192  40165  2sbc6g  40170  2sbc5g  40171  pm14.122b  40178  equncomVD  40627  csbingVD  40643  csbsngVD  40652  csbxpgVD  40653  csbresgVD  40654  csbrngVD  40655  csbima12gALTVD  40656  csbunigVD  40657  csbfv12gALTVD  40658  relopabVD  40660  dvnprodlem1  41667  dvnprodlem2  41668  dvnprodlem3  41669  dvnprod  41670  fourierdlem42  41871  etransclem11  41967  etransclem12  41968  etransclem33  41989  nnfoctbdjlem  42174  hoimbl  42350  aiota0def  42706  euoreqb  42720  funressndmafv2rn  42834  funressnbrafv2  42855  dfatbrafv2b  42856  funbrafv2  42858  fnbrafv2b  42859  fargshiftf1  42979  ichnreuop  43008  paireqne  43047  reupr  43058  uspgrsprf1  43396  uspgrsprfo  43397  lidldomn1  43562  nn0sumshdiglem2  44056  setrec2lem2  44170