Theorem eqeq2 2748

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  eqeq2i  2749  eqtr3  2758  clelab  2880  alexeqg  3605  pm13.183  3620  elab6g  3623  eqeu  3664  moeq3  3670  mo2icl  3672  mob2  3673  euind  3682  reu6i  3686  reu2eqd  3694  reuind  3711  sbc2or  3749  sbc5ALT  3769  csbiebg  3881  eqif  4521  sneq  4590  reusngf  4631  rexreusng  4636  reuprg0  4659  preq1b  4802  preq12bg  4809  preqsn  4818  disji2  5082  disjprg  5094  dtruALT  5333  opth  5424  euotd  5461  solin  5559  ideqg  5800  resieq  5949  cnveqb  6154  cnveq0  6155  reu3op  6250  reuop  6251  iota5  6475  funopg  6526  fneq2  6584  foeq3  6744  tz6.12f  6859  funbrfv  6882  fnbrfvb  6884  fvelimab  6906  elrnrexdm  7034  funsndifnop  7096  fconst5  7152  eufnfv  7175  f1veqaeq  7202  fpropnf1  7213  nf1const  7250  isosolem  7293  f1opr  7414  mpoeq123  7430  ovmpt4g  7505  ov3  7521  ovg  7523  caovcang  7559  caovcan  7562  tfisi  7801  tfindsg  7803  findsg  7839  f1oweALT  7916  seqomlem2  8382  oawordeu  8482  omopth  8590  ereq2  8643  qsdisj  8731  eroveu  8749  2dom  8967  fundmen  8968  xpf1o  9067  nneneq  9130  pwfir  9217  cantnflem1  9598  brttrcl  9622  ttrcltr  9625  ttrclss  9629  ttrclselem2  9635  updjud  9846  alephfp  10018  dfac5  10039  cardcf  10162  cfeq0  10166  sornom  10187  fpwwe2cbv  10541  fpwwe2lem3  10544  ltsosr  11005  map2psrpr  11021  axpre-lttri  11076  subval  11371  divval  11798  nn0ind-raph  12592  fvf1tp  13709  uzrdgfni  13881  sqeqor  14139  nn0opth2  14195  hashrabsn1  14297  elprchashprn2  14319  hashbclem  14375  hashbc  14376  hash2prde  14393  hash2pwpr  14399  brfi1indALT  14433  wrdind  14645  wrd2ind  14646  reuccatpfxs1lem  14669  cshf1  14733  wrdl3s3  14885  relexpindlem  14986  sqrtval  15160  sqrmo  15174  reusq0  15388  summolem2  15639  prodmolem2  15858  divides  16181  dvdstr  16221  odd2np1lem  16267  ndvdssub  16336  bitsinv1  16369  eucalglt  16512  hashgcdeq  16717  ramcl2lem  16937  ramcl  16957  cshwrepswhash1  17030  imasaddfnlem  17449  fnhomeqhomf  17614  initoeu2lem1  17938  cat1lem  18020  posi  18240  sgrp2nmndlem3  18850  dfgrp2  18892  grpidinv  18928  dfgrp3lem  18968  orbsta  19242  symgfvne  19310  symgfix2  19345  odlem1  19464  gexlem1  19508  slwispgp  19540  sylow3lem6  19561  efgrelexlemb  19679  gsumval3lem2  19835  pgpfac1  20011  pgpfaclem2  20013  pgpfac  20015  ablfaclem1  20016  isdomn  20638  isdomn4  20649  domnlcanb  20653  domnrcanb  20655  obsip  21676  uvcval  21740  mvrval  21937  mhpval  22082  psdfval  22101  psdmvr  22112  coe1tmmul2  22218  coe1tmmul  22219  mat1comp  22384  mat1dimid  22418  scmateALT  22456  marrepval  22506  marepvval  22511  minmar1val  22592  gsummatr01  22603  t0sep  23268  t1sep2  23313  is2ndc  23390  kqt0lem  23680  isr0  23681  isufil2  23852  xmeteq0  24282  imasf1oxmet  24319  xrsxmet  24754  iccpnfcnv  24898  dyadmax  25555  dyadmbl  25557  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  dvfsumlem1  25988  mdegle0  26038  fta1g  26131  ig1peu  26136  fta1  26272  aalioulem2  26297  taylthlem2  26338  efopn  26623  efrlim  26935  efrlimOLD  26936  musum  27157  mpodvdsmulf1o  27160  dvdsmulf1o  27162  dchrsum2  27235  sumdchr2  27237  gausslemma2dlem0i  27331  addsqnreup  27410  2sqreulem1  27413  2sqreultblem  27415  2sqreunnlem1  27416  2sqreunnltblem  27418  2sqreulem3  27420  ltsres  27630  nosupprefixmo  27668  noinfprefixmo  27669  nosupcbv  27670  nosupno  27671  nosupfv  27674  noinfcbv  27685  noinfno  27686  noinffv  27689  elmade  27853  divsval  28185  noseqrdgfn  28302  bdayn0sf1o  28366  bdayfinbndlem2  28464  axtgcgrid  28535  axtgbtwnid  28538  tglowdim1i  28573  islmib  28859  axcontlem12  29048  upgredgpr  29215  ushgredgedg  29302  ushgredgedgloop  29304  rusgrpropnb  29657  rgrx0ndm  29667  uspgr2wlkeq  29719  wlkson  29728  upgrwlkdvdelem  29809  spthonepeq  29825  iswwlksnon  29926  wlklnwwlkln2lem  29955  wwlksnredwwlkn  29968  wwlksnextprop  29985  wwlksnwwlksnon  29988  elwwlks2ons3  30028  rusgrnumwwlklem  30046  clwlkclwwlklem2a4  30072  clwwlkn  30101  clwwlkext2edg  30131  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  clwwlknon  30165  clwwlk0on0  30167  uhgr3cyclexlem  30256  1conngr  30269  frgr3vlem1  30348  3vfriswmgrlem  30352  frgrwopreglem3  30389  fusgreg2wsplem  30408  fusgreghash2wsp  30413  numclwlk1lem1  30444  numclwwlkovq  30449  numclwwlk2lem1  30451  frgrregord013  30470  friendshipgt3  30473  ex-opab  30507  isgrpoi  30573  grpoidinv2  30590  hvsubeq0  31143  hvaddcan  31145  hvsubadd  31152  normsub0  31211  omlsi  31479  pjoml  31511  nonbooli  31726  pj11  31789  lnopeq  32084  nmopun  32089  pjclem4a  32273  pj3lem1  32281  strlem4  32329  hstrlem4  32337  jplem1  32343  superpos  32429  ifeqeqx  32617  disji2f  32652  disjif2  32656  disjabrex  32657  disjabrexf  32658  disjxpin  32663  disjunsn  32669  ofpreima  32743  fgreu  32750  fcnvgreu  32751  sgnsub  32918  gsumhashmul  33150  elrgspnlem2  33325  elrgspnlem3  33326  elrgspnlem4  33327  domnlcanOLD  33362  ismxidl  33543  mplmulmvr  33704  esplyfval  33721  esplyfval0  33722  esplyfv  33728  esplyfval3  33730  xrge0iifcnv  34090  esumpr2  34224  eulerpartlemgvv  34533  eulerpartlemgh  34535  eulerpartlemgs2  34537  plymulx0  34704  lpadmax  34839  lpadright  34841  bnj1321  35183  f1resfz0f1d  35308  subfacp1lem3  35376  pconncn  35418  cnpconn  35424  txpconn  35426  connpconn  35429  cvmlift3lem2  35514  cvmlift3lem4  35516  cvmlift3  35522  snmlflim  35526  iota5f  35918  rankeq1o  36365  nn0prpw  36517  bj-csbsnlem  37104  bj-elgab  37140  bj-restsnss  37288  bj-restsnss2  37289  bj-imdirco  37395  wl-isseteq  37710  wl-ax12v2cl  37711  fin2so  37808  poimirlem2  37823  poimirlem18  37839  poimirlem21  37842  poimirlem25  37846  poimirlem26  37847  poimirlem27  37848  mblfinlem2  37859  mbfresfi  37867  cnambfre  37869  ftc1anclem8  37901  fdc  37946  istotbnd  37970  isexid2  38056  isgrpda  38156  ismaxidl  38241  mpobi123f  38363  mptbi12f  38367  disjressuc2  38596  qsdisjALTV  38872  parteq2  39034  lsatcmp  39263  lshpkrlem1  39370  trlval2  40423  cdlemg1cex  40848  cdlemm10N  41378  dicval  41436  lcmineqlem4  42286  grpods  42448  unitscyglem2  42450  unitscyglem3  42451  unitscyglem4  42452  exfinfldd  42457  nnn1suc  42521  resubval  42622  redivvald  42697  fsuppind  42833  unxpwdom3  43337  dgraalem  43387  dgraaub  43390  onsucf1lem  43511  frege104  44208  pm13.192  44651  2sbc6g  44656  2sbc5g  44657  pm14.122b  44664  equncomVD  45108  csbingVD  45124  csbsngVD  45133  csbxpgVD  45134  csbresgVD  45135  csbrngVD  45136  csbima12gALTVD  45137  csbunigVD  45138  csbfv12gALTVD  45139  relopabVD  45141  dvnprodlem1  46190  dvnprodlem2  46191  dvnprodlem3  46192  dvnprod  46193  fourierdlem42  46393  etransclem11  46489  etransclem12  46490  etransclem33  46511  nnfoctbdjlem  46699  hoimbl  46875  cfsetsnfsetf  47304  aiota0def  47342  euoreqb  47355  funressndmafv2rn  47469  funressnbrafv2  47490  dfatbrafv2b  47491  funbrafv2  47493  fnbrafv2b  47494  elsetpreimafvbi  47637  elsetpreimafveq  47643  imasetpreimafvbijlemfo  47651  fargshiftf1  47687  ichnreuop  47718  paireqne  47757  reupr  47768  isuspgrim0  48140  upgrimpths  48155  clnbgrgrim  48180  grimedg  48181  isubgr3stgrlem4  48215  isubgr3stgrlem7  48218  gpgedg2ov  48312  gpgedg2iv  48313  pgnbgreunbgrlem1  48359  pgnbgreunbgrlem2lem3  48362  pgnbgreunbgrlem4  48365  pgnbgreunbgr  48371  uspgrsprf1  48393  uspgrsprfo  48394  lidldomn1  48477  nn0sumshdiglem2  48868  mof0  49083  eufsnlem  49086  oppcmndclem  49262  isthincd2lem1  49670  termcbasmo  49728  termcarweu  49773  arweuthinc  49774  arweutermc  49775  setrec2lem2  49939