Theorem eqeq2 2621

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  eqeq2i  2622  eqeq12  2623  alexeqg  3302  pm13.183  3313  eqeu  3344  moeq3  3350  mo2icl  3352  mob2  3353  euind  3360  reu6i  3364  reu2eqd  3370  reuind  3378  sbc2or  3411  sbc5  3427  csbiebg  3522  eqif  4076  sneq  4135  preq1b  4317  preqr1OLD  4320  prel12  4323  preq12bg  4326  prel12g  4327  preqsn  4331  disji2  4569  disjprg  4578  dtruALT  4826  dtruALT2  4838  opth  4871  euotd  4900  solin  4982  ideqg  5195  resieq  5327  cnveqb  5508  cnveq0  5509  iota5  5788  funopg  5836  fneq2  5894  foeq3  6026  tz6.12f  6122  funbrfv  6144  fnbrfvb  6146  fvelimab  6163  elrnrexdm  6271  funsndifnop  6321  fconst5  6376  eufnfv  6395  f1veqaeq  6418  isosolem  6497  mpt2eq123  6612  ovmpt4g  6681  ov3  6695  ovg  6697  caovcang  6733  caovcan  6736  tfisi  6950  tfindsg  6952  findsg  6985  f1oweALT  7043  seqomlem2  7433  oawordeu  7522  omopth  7625  ereq2  7637  qsdisj  7711  eroveu  7729  2dom  7915  fundmen  7916  xpf1o  8007  nneneq  8028  cantnflem1  8469  alephfp  8814  dfac5  8834  cardcf  8957  cfeq0  8961  sornom  8982  fpwwe2cbv  9331  fpwwe2lem3  9334  ltsosr  9794  map2psrpr  9810  axpre-lttri  9865  subval  10151  divval  10566  nn0ind-raph  11353  uzrdgfni  12619  sqeqor  12840  nn0opth2  12921  hashrabsn1  13024  elprchashprn2  13045  hashbclem  13093  hashbc  13094  hash2prde  13109  hash2pwpr  13115  fundmge2nop0  13129  brfi1indALT  13137  brfi1indALTOLD  13143  wrdind  13328  wrd2ind  13329  reuccats1lem  13331  cshf1  13407  wrdl3s3  13553  relexpindlem  13651  sqrtval  13825  sqrmo  13840  summolem2  14294  prodmolem2  14504  divides  14823  dvdstr  14856  odd2np1lem  14902  ndvdssub  14971  bitsinv1  15002  eucalglt  15136  hashgcdeq  15332  ramcl2lem  15551  ramcl  15571  cshwrepswhash1  15647  imasaddfnlem  16011  fnhomeqhomf  16174  initoeu2lem1  16487  posi  16773  sgrp2nmndlem3  17235  dfgrp2  17270  grpidinv  17298  dfgrp3lem  17336  orbsta  17569  symgfvne  17631  symgfix2  17659  odlem1  17777  gexlem1  17817  slwispgp  17849  sylow3lem6  17870  efgrelexlemb  17986  gsumval3lem2  18130  pgpfac1  18302  pgpfaclem2  18304  pgpfac  18306  ablfaclem1  18307  isdomn  19115  mvrval  19242  coe1tmmul2  19467  coe1tmmul  19468  obsip  19884  uvcval  19943  mat1comp  20065  mat1dimid  20099  scmateALT  20137  marrepval  20187  marepvval  20192  minmar1val  20273  gsummatr01  20284  t0sep  20938  t1sep2  20983  is2ndc  21059  kqt0lem  21349  isr0  21350  isufil2  21522  xmeteq0  21953  imasf1oxmet  21990  xrsxmet  22420  iccpnfcnv  22551  dyadmax  23172  dyadmbl  23174  dvfsumle  23588  dvfsumabs  23590  dvfsumlem1  23593  mdegle0  23641  fta1g  23731  ig1peu  23735  fta1  23867  aalioulem2  23892  efopn  24204  efrlim  24496  musum  24717  dvdsmulf1o  24720  dchrsum2  24793  sumdchr2  24795  gausslemma2dlem0i  24889  axtgcgrid  25162  axtgbtwnid  25165  tglowdim1i  25196  islmib  25479  axcontlem12  25655  upgredgpr  25815  wlkon  26061  wlkntrllem3  26091  spthonepeq  26117  fargshiftf1  26165  constr3trllem2  26179  wlklniswwlkn2  26228  usg2wlkeq  26236  wwlknredwwlkn  26254  wwlkextprop  26272  clwwlkn  26295  clwlkisclwwlklem2a4  26312  clwwlkext2edg  26330  clwwnisshclwwn  26337  hashecclwwlkn1  26361  usghashecclwwlk  26362  clwlkfoclwwlk  26372  2wlkonot  26392  2spthonot  26393  el2wlkonot  26396  el2spthonot  26397  el2spthonot0  26398  rusgraprop2  26469  rusgrasn  26472  rusgranumwlklem1  26476  rusgranumwlklem2  26477  rusgranumwlklem3  26478  rusgranumwlkg  26485  clwlknclwlkdifs  26487  frgra3vlem1  26527  3vfriswmgralem  26531  usg2spot2nb  26592  usgreg2spot  26594  2spotmdisj  26595  usgreghash2spot  26596  numclwwlkun  26606  numclwwlkdisj  26607  numclwwlkovf  26608  numclwwlkovg  26614  numclwlk1lem2f1  26621  numclwwlkovq  26626  numclwwlkovh  26628  numclwwlk5  26639  frgrareg  26644  frgraregord013  26645  friendshipgt3  26648  ex-opab  26681  isgrpoi  26736  grpoidinv2  26753  hvsubeq0  27309  hvaddcan  27311  hvsubadd  27318  normsub0  27377  omlsi  27647  pjoml  27679  nonbooli  27894  pj11  27957  lnopeq  28252  nmopun  28257  pjclem4a  28441  pj3lem1  28449  strlem4  28497  hstrlem4  28505  jplem1  28511  superpos  28597  rmoeqALT  28711  ifeqeqx  28745  disji2f  28772  disjif2  28776  disjabrex  28777  disjabrexf  28778  disjxpin  28783  disjunsn  28789  ofpreima  28848  fgreu  28854  fcnvgreu  28855  xrge0iifcnv  29307  esumpr2  29456  eulerpartlemgvv  29765  eulerpartlemgh  29767  eulerpartlemgs2  29769  sgnsub  29933  plymulx0  29950  bnj1321  30349  subfacp1lem3  30418  pconcn  30460  cnpcon  30466  txpcon  30468  conpcon  30471  cvmlift3lem2  30556  cvmlift3lem4  30558  cvmlift3  30564  snmlflim  30568  iota5f  30861  br1steqg  30919  br2ndeqg  30920  sltres  31061  nofulllem5  31105  rankeq1o  31448  nn0prpw  31488  bj-csbsnlem  32090  bj-restsnss  32217  bj-restsnss2  32218  fin2so  32566  poimirlem2  32581  poimirlem18  32597  poimirlem21  32600  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  mblfinlem2  32617  mbfresfi  32626  cnambfre  32628  ftc1anclem8  32662  f1opr  32689  fdc  32711  istotbnd  32738  isexid2  32824  isgrpda  32924  ismaxidl  33009  mpt2bi123f  33141  mptbi12f  33145  lsatcmp  33308  lshpkrlem1  33415  trlval2  34468  cdlemg1cex  34894  cdlemm10N  35425  dicval  35483  unxpwdom3  36683  dgraalem  36734  dgraaub  36737  frege104  37281  pm13.192  37633  2sbc6g  37638  2sbc5g  37639  pm14.122b  37646  equncomVD  38126  csbingVD  38142  csbsngVD  38151  csbxpgVD  38152  csbresgVD  38153  csbrngVD  38154  csbima12gALTVD  38155  csbunigVD  38156  csbfv12gALTVD  38157  relopabVD  38159  dvnprodlem1  38836  dvnprodlem2  38837  dvnprodlem3  38838  dvnprod  38839  fourierdlem42  39042  etransclem11  39138  etransclem12  39139  etransclem33  39160  nnfoctbdjlem  39348  hoimbl  39521  reuccatpfxs1lem  40296  clel5  40303  fpropnf1  40337  ushgredgedga  40456  ushgredgedgaloop  40458  rusgrpropnb  40783  rgrx0ndm  40793  uspgr2wlkeq  40854  wlkson  40864  upgrwlkdvdelem  40942  spthonepeq-av  40958  iswwlksnon  41051  1wlklnwwlkln2lem  41079  wwlksnredwwlkn  41101  wwlksnextprop  41118  wwlksnwwlksnon  41121  wwlks2onv  41158  elwwlks2ons3  41159  rusgrnumwwlklem  41173  clwwlknclwwlkdifs  41181  clwwlksn  41189  clwlkclwwlklem2a4  41206  clwwlksext2edg  41230  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  clwlksfoclwwlk  41270  clwwlksndisj  41280  uhgr3cyclexlem  41348  1conngr  41361  frgr3vlem1  41443  3vfriswmgrlem  41447  frgr2wwlkeqm  41496  fusgr2wsp2nb  41498  fusgreg2wsp  41500  2wspmdisj  41501  fusgreghash2wsp  41502  av-numclwwlkovf  41511  av-numclwwlkovg  41518  av-numclwlk1lem2f1  41524  av-numclwwlkovq  41529  av-numclwwlkovh  41531  av-numclwwlk2lem1  41532  av-numclwwlk5  41542  av-frgraregord013  41549  av-friendshipgt3  41552  lidldomn1  41711  nn0sumshdiglem2  42214  setrec2lem2  42240