Theorem eqeq2 2750

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730

This theorem is referenced by:  eqeq2i  2751  eqeq12OLD  2757  eqtr3  2764  clelab  2883  alexeqg  3582  pm13.183  3598  elab6g  3601  eqeu  3642  moeq3  3648  mo2icl  3650  mob2  3651  euind  3660  reu6i  3664  reu2eqd  3672  reuind  3689  sbc2or  3726  sbc5ALT  3746  csbiebg  3866  eqif  4502  sneq  4573  reusngf  4610  rexreusng  4617  reuprg0  4640  preq1b  4779  preq12bg  4786  preqsn  4794  disji2  5057  disjprgw  5070  disjprg  5071  dtruALT  5311  opth  5391  euotd  5427  solin  5525  ideqg  5755  resieq  5897  cnveqb  6094  cnveq0  6095  reu3op  6190  reuop  6191  iota5  6411  funopg  6462  fneq2  6519  foeq3  6680  tz6.12f  6792  funbrfv  6814  fnbrfvb  6816  fvelimab  6835  elrnrexdm  6959  funsndifnop  7017  fconst5  7075  eufnfv  7099  f1veqaeq  7124  fpropnf1  7134  nf1const  7170  isosolem  7212  f1opr  7323  mpoeq123  7339  ovmpt4g  7412  ov3  7427  ovg  7429  caovcang  7465  caovcan  7468  tfisi  7697  tfindsg  7699  findsg  7738  f1oweALT  7806  seqomlem2  8271  oawordeu  8375  omopth  8481  ereq2  8495  qsdisj  8572  eroveu  8590  2dom  8809  fundmen  8810  xpf1o  8915  pwfir  8948  nneneq  8981  nneneqOLD  8993  cantnflem1  9436  brttrcl  9460  ttrcltr  9463  ttrclss  9467  ttrclselem2  9473  updjud  9681  alephfp  9853  dfac5  9873  cardcf  9997  cfeq0  10001  sornom  10022  fpwwe2cbv  10375  fpwwe2lem3  10378  ltsosr  10839  map2psrpr  10855  axpre-lttri  10910  subval  11201  divval  11624  nn0ind-raph  12409  uzrdgfni  13667  sqeqor  13921  nn0opth2  13975  hashrabsn1  14078  elprchashprn2  14100  hashbclem  14153  hashbc  14154  hash2prde  14173  hash2pwpr  14179  brfi1indALT  14203  wrdind  14424  wrd2ind  14425  reuccatpfxs1lem  14448  cshf1  14512  wrdl3s3  14666  relexpindlem  14763  sqrtval  14937  sqrmo  14952  reusq0  15163  summolem2  15417  prodmolem2  15634  divides  15954  dvdstr  15992  odd2np1lem  16038  ndvdssub  16107  bitsinv1  16138  eucalglt  16279  hashgcdeq  16479  ramcl2lem  16699  ramcl  16719  cshwrepswhash1  16793  imasaddfnlem  17228  fnhomeqhomf  17389  initoeu2lem1  17718  cat1lem  17800  posi  18024  sgrp2nmndlem3  18553  dfgrp2  18593  grpidinv  18624  dfgrp3lem  18662  orbsta  18908  symgfvne  18977  symgfix2  19013  odlem1  19132  gexlem1  19173  slwispgp  19205  sylow3lem6  19226  efgrelexlemb  19345  gsumval3lem2  19496  pgpfac1  19672  pgpfaclem2  19674  pgpfac  19676  ablfaclem1  19677  isdomn  20554  obsip  20917  uvcval  20981  mvrval  21179  mhpval  21319  coe1tmmul2  21436  coe1tmmul  21437  mat1comp  21578  mat1dimid  21612  scmateALT  21650  marrepval  21700  marepvval  21705  minmar1val  21786  gsummatr01  21797  t0sep  22464  t1sep2  22509  is2ndc  22586  kqt0lem  22876  isr0  22877  isufil2  23048  xmeteq0  23480  imasf1oxmet  23517  xrsxmet  23961  iccpnfcnv  24096  dyadmax  24751  dyadmbl  24753  dvfsumle  25174  dvfsumabs  25176  dvfsumlem1  25179  mdegle0  25231  fta1g  25321  ig1peu  25325  fta1  25457  aalioulem2  25482  efopn  25802  efrlim  26108  musum  26329  dvdsmulf1o  26332  dchrsum2  26405  sumdchr2  26407  gausslemma2dlem0i  26501  addsqnreup  26580  2sqreulem1  26583  2sqreultblem  26585  2sqreunnlem1  26586  2sqreunnltblem  26588  2sqreulem3  26590  axtgcgrid  26813  axtgbtwnid  26816  tglowdim1i  26851  islmib  27137  axcontlem12  27332  upgredgpr  27501  ushgredgedg  27585  ushgredgedgloop  27587  rusgrpropnb  27939  rgrx0ndm  27949  uspgr2wlkeq  28001  wlkson  28012  upgrwlkdvdelem  28091  spthonepeq  28107  iswwlksnon  28205  wlklnwwlkln2lem  28234  wwlksnredwwlkn  28247  wwlksnextprop  28264  wwlksnwwlksnon  28267  elwwlks2ons3  28307  rusgrnumwwlklem  28322  clwlkclwwlklem2a4  28348  clwwlkn  28377  clwwlkext2edg  28407  hashecclwwlkn1  28428  umgrhashecclwwlk  28429  clwwlknon  28441  clwwlk0on0  28443  uhgr3cyclexlem  28532  1conngr  28545  frgr3vlem1  28624  3vfriswmgrlem  28628  frgrwopreglem3  28665  fusgreg2wsplem  28684  fusgreghash2wsp  28689  numclwlk1lem1  28720  numclwwlkovq  28725  numclwwlk2lem1  28727  frgrregord013  28746  friendshipgt3  28749  ex-opab  28783  isgrpoi  28847  grpoidinv2  28864  hvsubeq0  29417  hvaddcan  29419  hvsubadd  29426  normsub0  29485  omlsi  29753  pjoml  29785  nonbooli  30000  pj11  30063  lnopeq  30358  nmopun  30363  pjclem4a  30547  pj3lem1  30555  strlem4  30603  hstrlem4  30611  jplem1  30617  superpos  30703  ifeqeqx  30872  disji2f  30903  disjif2  30907  disjabrex  30908  disjabrexf  30909  disjxpin  30914  disjunsn  30920  ofpreima  30989  fgreu  30996  fcnvgreu  30997  gsumhashmul  31303  ismxidl  31621  xrge0iifcnv  31870  esumpr2  32022  eulerpartlemgvv  32330  eulerpartlemgh  32332  eulerpartlemgs2  32334  sgnsub  32498  plymulx0  32513  lpadmax  32649  lpadright  32651  bnj1321  32994  f1resfz0f1d  33059  subfacp1lem3  33131  pconncn  33173  cnpconn  33179  txpconn  33181  connpconn  33184  cvmlift3lem2  33269  cvmlift3lem4  33271  cvmlift3  33277  snmlflim  33281  iota5f  33656  sltres  33852  nosupprefixmo  33890  noinfprefixmo  33891  nosupcbv  33892  nosupno  33893  nosupfv  33896  noinfcbv  33907  noinfno  33908  noinffv  33911  elmade  34038  rankeq1o  34460  nn0prpw  34499  bj-csbsnlem  35075  bj-elgab  35114  bj-restsnss  35241  bj-restsnss2  35242  bj-imdirco  35348  fin2so  35751  poimirlem2  35766  poimirlem18  35782  poimirlem21  35785  poimirlem25  35789  poimirlem26  35790  poimirlem27  35791  mblfinlem2  35802  mbfresfi  35810  cnambfre  35812  ftc1anclem8  35844  fdc  35890  istotbnd  35914  isexid2  36000  isgrpda  36100  ismaxidl  36185  mpobi123f  36307  mptbi12f  36311  qsdisjALTV  36715  lsatcmp  37004  lshpkrlem1  37111  trlval2  38164  cdlemg1cex  38589  cdlemm10N  39119  dicval  39177  lcmineqlem4  40027  isdomn4  40159  fsuppind  40266  nnn1suc  40283  resubval  40337  unxpwdom3  40907  dgraalem  40957  dgraaub  40960  frege104  41535  pm13.192  41988  2sbc6g  41993  2sbc5g  41994  pm14.122b  42001  equncomVD  42448  csbingVD  42464  csbsngVD  42473  csbxpgVD  42474  csbresgVD  42475  csbrngVD  42476  csbima12gALTVD  42477  csbunigVD  42478  csbfv12gALTVD  42479  relopabVD  42481  dvnprodlem1  43447  dvnprodlem2  43448  dvnprodlem3  43449  dvnprod  43450  fourierdlem42  43650  etransclem11  43746  etransclem12  43747  etransclem33  43768  nnfoctbdjlem  43953  hoimbl  44129  cfsetsnfsetf  44509  aiota0def  44545  euoreqb  44558  funressndmafv2rn  44672  funressnbrafv2  44693  dfatbrafv2b  44694  funbrafv2  44696  fnbrafv2b  44697  elsetpreimafvbi  44800  elsetpreimafveq  44806  imasetpreimafvbijlemfo  44814  fargshiftf1  44850  ichnreuop  44881  paireqne  44920  reupr  44931  uspgrsprf1  45266  uspgrsprfo  45267  lidldomn1  45436  nn0sumshdiglem2  45925  mof0  46122  eufsnlem  46125  isthincd2lem1  46265  setrec2lem2  46357