Theorem eqeq2 2810

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  eqeq2i  2811  eqeq12  2812  alexeqg  3592  pm13.183  3606  eqeu  3645  moeq3  3651  mo2icl  3653  mob2  3654  euind  3663  reu6i  3667  reu2eqd  3675  reuind  3692  sbc2or  3729  sbc5  3748  csbiebg  3860  eqif  4465  sneq  4535  reusngf  4572  rexreusng  4577  reuprg0  4598  preq1b  4737  preq12bg  4744  preqsn  4752  disji2  5012  disjprgw  5025  disjprg  5026  dtruALT  5254  dtruALT2  5301  opth  5333  euotd  5368  solin  5462  ideqg  5686  resieq  5829  cnveqb  6020  cnveq0  6021  reu3op  6111  reuop  6112  iota5  6307  funopg  6358  fneq2  6415  foeq3  6563  tz6.12f  6669  funbrfv  6691  fnbrfvb  6693  fvelimab  6712  elrnrexdm  6832  funsndifnop  6890  fconst5  6945  eufnfv  6969  f1veqaeq  6993  fpropnf1  7003  nf1const  7038  isosolem  7079  f1opr  7189  mpoeq123  7205  ovmpt4g  7276  ov3  7291  ovg  7293  caovcang  7329  caovcan  7332  tfisi  7553  tfindsg  7555  findsg  7590  f1oweALT  7655  seqomlem2  8070  oawordeu  8164  omopth  8268  ereq2  8280  qsdisj  8357  eroveu  8375  2dom  8565  fundmen  8566  xpf1o  8663  nneneq  8684  cantnflem1  9136  updjud  9347  alephfp  9519  dfac5  9539  cardcf  9663  cfeq0  9667  sornom  9688  fpwwe2cbv  10041  fpwwe2lem3  10044  ltsosr  10505  map2psrpr  10521  axpre-lttri  10576  subval  10866  divval  11289  nn0ind-raph  12070  uzrdgfni  13321  sqeqor  13574  nn0opth2  13628  hashrabsn1  13731  elprchashprn2  13753  hashbclem  13806  hashbc  13807  hash2prde  13824  hash2pwpr  13830  brfi1indALT  13854  wrdind  14075  wrd2ind  14076  reuccatpfxs1lem  14099  cshf1  14163  wrdl3s3  14317  relexpindlem  14414  sqrtval  14588  sqrmo  14603  reusq0  14814  summolem2  15065  prodmolem2  15281  divides  15601  dvdstr  15638  odd2np1lem  15681  ndvdssub  15750  bitsinv1  15781  eucalglt  15919  hashgcdeq  16116  ramcl2lem  16335  ramcl  16355  cshwrepswhash1  16428  imasaddfnlem  16793  fnhomeqhomf  16953  initoeu2lem1  17266  posi  17552  sgrp2nmndlem3  18082  dfgrp2  18120  grpidinv  18151  dfgrp3lem  18189  orbsta  18435  symgfvne  18501  symgfix2  18536  odlem1  18655  gexlem1  18696  slwispgp  18728  sylow3lem6  18749  efgrelexlemb  18868  gsumval3lem2  19019  pgpfac1  19195  pgpfaclem2  19197  pgpfac  19199  ablfaclem1  19200  isdomn  20060  obsip  20410  uvcval  20474  mvrval  20659  mhpval  20792  coe1tmmul2  20905  coe1tmmul  20906  mat1comp  21045  mat1dimid  21079  scmateALT  21117  marrepval  21167  marepvval  21172  minmar1val  21253  gsummatr01  21264  t0sep  21929  t1sep2  21974  is2ndc  22051  kqt0lem  22341  isr0  22342  isufil2  22513  xmeteq0  22945  imasf1oxmet  22982  xrsxmet  23414  iccpnfcnv  23549  dyadmax  24202  dyadmbl  24204  dvfsumle  24624  dvfsumabs  24626  dvfsumlem1  24629  mdegle0  24678  fta1g  24768  ig1peu  24772  fta1  24904  aalioulem2  24929  efopn  25249  efrlim  25555  musum  25776  dvdsmulf1o  25779  dchrsum2  25852  sumdchr2  25854  gausslemma2dlem0i  25948  addsqnreup  26027  2sqreulem1  26030  2sqreultblem  26032  2sqreunnlem1  26033  2sqreunnltblem  26035  2sqreulem3  26037  axtgcgrid  26257  axtgbtwnid  26260  tglowdim1i  26295  islmib  26581  axcontlem12  26769  upgredgpr  26935  ushgredgedg  27019  ushgredgedgloop  27021  rusgrpropnb  27373  rgrx0ndm  27383  uspgr2wlkeq  27435  wlkson  27446  upgrwlkdvdelem  27525  spthonepeq  27541  iswwlksnon  27639  wlklnwwlkln2lem  27668  wwlksnredwwlkn  27681  wwlksnextprop  27698  wwlksnwwlksnon  27701  elwwlks2ons3  27741  rusgrnumwwlklem  27756  clwlkclwwlklem2a4  27782  clwwlkn  27811  clwwlkext2edg  27841  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  clwwlknon  27875  clwwlk0on0  27877  uhgr3cyclexlem  27966  1conngr  27979  frgr3vlem1  28058  3vfriswmgrlem  28062  frgrwopreglem3  28099  fusgreg2wsplem  28118  fusgreghash2wsp  28123  numclwlk1lem1  28154  numclwwlkovq  28159  numclwwlk2lem1  28161  frgrregord013  28180  friendshipgt3  28183  ex-opab  28217  isgrpoi  28281  grpoidinv2  28298  hvsubeq0  28851  hvaddcan  28853  hvsubadd  28860  normsub0  28919  omlsi  29187  pjoml  29219  nonbooli  29434  pj11  29497  lnopeq  29792  nmopun  29797  pjclem4a  29981  pj3lem1  29989  strlem4  30037  hstrlem4  30045  jplem1  30051  superpos  30137  ifeqeqx  30309  disji2f  30340  disjif2  30344  disjabrex  30345  disjabrexf  30346  disjxpin  30351  disjunsn  30357  ofpreima  30428  fgreu  30435  fcnvgreu  30436  gsumhashmul  30741  ismxidl  31042  xrge0iifcnv  31286  esumpr2  31436  eulerpartlemgvv  31744  eulerpartlemgh  31746  eulerpartlemgs2  31748  sgnsub  31912  plymulx0  31927  lpadmax  32063  lpadright  32065  bnj1321  32409  f1resfz0f1d  32471  subfacp1lem3  32542  pconncn  32584  cnpconn  32590  txpconn  32592  connpconn  32595  cvmlift3lem2  32680  cvmlift3lem4  32682  cvmlift3  32688  snmlflim  32692  iota5f  33068  sltres  33282  noprefixmo  33315  nosupno  33316  nosupfv  33319  rankeq1o  33745  nn0prpw  33784  bj-csbsnlem  34344  bj-restsnss  34498  bj-restsnss2  34499  bj-imdirco  34605  fin2so  35044  poimirlem2  35059  poimirlem18  35075  poimirlem21  35078  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  mblfinlem2  35095  mbfresfi  35103  cnambfre  35105  ftc1anclem8  35137  fdc  35183  istotbnd  35207  isexid2  35293  isgrpda  35393  ismaxidl  35478  mpobi123f  35600  mptbi12f  35604  qsdisjALTV  36010  lsatcmp  36299  lshpkrlem1  36406  trlval2  37459  cdlemg1cex  37884  cdlemm10N  38414  dicval  38472  lcmineqlem4  39320  fsuppind  39456  nnn1suc  39467  resubval  39505  unxpwdom3  40039  dgraalem  40089  dgraaub  40092  frege104  40668  pm13.192  41114  2sbc6g  41119  2sbc5g  41120  pm14.122b  41127  equncomVD  41574  csbingVD  41590  csbsngVD  41599  csbxpgVD  41600  csbresgVD  41601  csbrngVD  41602  csbima12gALTVD  41603  csbunigVD  41604  csbfv12gALTVD  41605  relopabVD  41607  dvnprodlem1  42588  dvnprodlem2  42589  dvnprodlem3  42590  dvnprod  42591  fourierdlem42  42791  etransclem11  42887  etransclem12  42888  etransclem33  42909  nnfoctbdjlem  43094  hoimbl  43270  aiota0def  43651  euoreqb  43665  funressndmafv2rn  43779  funressnbrafv2  43800  dfatbrafv2b  43801  funbrafv2  43803  fnbrafv2b  43804  elsetpreimafvbi  43908  elsetpreimafveq  43914  imasetpreimafvbijlemfo  43922  fargshiftf1  43958  ichnreuop  43989  paireqne  44028  reupr  44039  uspgrsprf1  44375  uspgrsprfo  44376  lidldomn1  44545  nn0sumshdiglem2  45036  setrec2lem2  45224