Theorem eqeq2 2741

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  eqeq2i  2742  eqtr3  2751  clelab  2873  alexeqg  3606  pm13.183  3621  elab6g  3624  eqeu  3666  moeq3  3672  mo2icl  3674  mob2  3675  euind  3684  reu6i  3688  reu2eqd  3696  reuind  3713  sbc2or  3751  sbc5ALT  3771  csbiebg  3883  eqif  4518  sneq  4587  reusngf  4626  rexreusng  4631  reuprg0  4654  preq1b  4797  preq12bg  4804  preqsn  4813  disji2  5076  disjprg  5088  dtruALT  5327  opth  5419  euotd  5456  solin  5554  ideqg  5794  resieq  5941  cnveqb  6145  cnveq0  6146  reu3op  6240  reuop  6241  iota5  6465  funopg  6516  fneq2  6574  foeq3  6734  tz6.12f  6847  funbrfv  6871  fnbrfvb  6873  fvelimab  6895  elrnrexdm  7023  funsndifnop  7085  fconst5  7142  eufnfv  7165  f1veqaeq  7193  fpropnf1  7204  nf1const  7241  isosolem  7284  f1opr  7405  mpoeq123  7421  ovmpt4g  7496  ov3  7512  ovg  7514  caovcang  7550  caovcan  7553  tfisi  7792  tfindsg  7794  findsg  7830  f1oweALT  7907  seqomlem2  8373  oawordeu  8473  omopth  8580  ereq2  8633  qsdisj  8721  eroveu  8739  2dom  8955  fundmen  8956  xpf1o  9056  nneneq  9120  pwfir  9206  cantnflem1  9585  brttrcl  9609  ttrcltr  9612  ttrclss  9616  ttrclselem2  9622  updjud  9830  alephfp  10002  dfac5  10023  cardcf  10146  cfeq0  10150  sornom  10171  fpwwe2cbv  10524  fpwwe2lem3  10527  ltsosr  10988  map2psrpr  11004  axpre-lttri  11059  subval  11354  divval  11781  nn0ind-raph  12576  fvf1tp  13693  uzrdgfni  13865  sqeqor  14123  nn0opth2  14179  hashrabsn1  14281  elprchashprn2  14303  hashbclem  14359  hashbc  14360  hash2prde  14377  hash2pwpr  14383  brfi1indALT  14417  wrdind  14628  wrd2ind  14629  reuccatpfxs1lem  14652  cshf1  14716  wrdl3s3  14869  relexpindlem  14970  sqrtval  15144  sqrmo  15158  reusq0  15372  summolem2  15623  prodmolem2  15842  divides  16165  dvdstr  16205  odd2np1lem  16251  ndvdssub  16320  bitsinv1  16353  eucalglt  16496  hashgcdeq  16701  ramcl2lem  16921  ramcl  16941  cshwrepswhash1  17014  imasaddfnlem  17432  fnhomeqhomf  17597  initoeu2lem1  17921  cat1lem  18003  posi  18223  sgrp2nmndlem3  18799  dfgrp2  18841  grpidinv  18877  dfgrp3lem  18917  orbsta  19192  symgfvne  19260  symgfix2  19295  odlem1  19414  gexlem1  19458  slwispgp  19490  sylow3lem6  19511  efgrelexlemb  19629  gsumval3lem2  19785  pgpfac1  19961  pgpfaclem2  19963  pgpfac  19965  ablfaclem1  19966  isdomn  20590  isdomn4  20601  domnlcanb  20605  domnrcanb  20607  obsip  21628  uvcval  21692  mvrval  21889  mhpval  22024  psdfval  22043  psdmvr  22054  coe1tmmul2  22160  coe1tmmul  22161  mat1comp  22325  mat1dimid  22359  scmateALT  22397  marrepval  22447  marepvval  22452  minmar1val  22533  gsummatr01  22544  t0sep  23209  t1sep2  23254  is2ndc  23331  kqt0lem  23621  isr0  23622  isufil2  23793  xmeteq0  24224  imasf1oxmet  24261  xrsxmet  24696  iccpnfcnv  24840  dyadmax  25497  dyadmbl  25499  dvfsumle  25924  dvfsumleOLD  25925  dvfsumabs  25927  dvfsumlem1  25930  mdegle0  25980  fta1g  26073  ig1peu  26078  fta1  26214  aalioulem2  26239  taylthlem2  26280  efopn  26565  efrlim  26877  efrlimOLD  26878  musum  27099  mpodvdsmulf1o  27102  dvdsmulf1o  27104  dchrsum2  27177  sumdchr2  27179  gausslemma2dlem0i  27273  addsqnreup  27352  2sqreulem1  27355  2sqreultblem  27357  2sqreunnlem1  27358  2sqreunnltblem  27360  2sqreulem3  27362  sltres  27572  nosupprefixmo  27610  noinfprefixmo  27611  nosupcbv  27612  nosupno  27613  nosupfv  27616  noinfcbv  27627  noinfno  27628  noinffv  27631  elmade  27781  divsval  28097  noseqrdgfn  28205  bdayn0sf1o  28264  axtgcgrid  28408  axtgbtwnid  28411  tglowdim1i  28446  islmib  28732  axcontlem12  28920  upgredgpr  29087  ushgredgedg  29174  ushgredgedgloop  29176  rusgrpropnb  29529  rgrx0ndm  29539  uspgr2wlkeq  29591  wlkson  29600  upgrwlkdvdelem  29681  spthonepeq  29697  iswwlksnon  29798  wlklnwwlkln2lem  29827  wwlksnredwwlkn  29840  wwlksnextprop  29857  wwlksnwwlksnon  29860  elwwlks2ons3  29900  rusgrnumwwlklem  29915  clwlkclwwlklem2a4  29941  clwwlkn  29970  clwwlkext2edg  30000  hashecclwwlkn1  30021  umgrhashecclwwlk  30022  clwwlknon  30034  clwwlk0on0  30036  uhgr3cyclexlem  30125  1conngr  30138  frgr3vlem1  30217  3vfriswmgrlem  30221  frgrwopreglem3  30258  fusgreg2wsplem  30277  fusgreghash2wsp  30282  numclwlk1lem1  30313  numclwwlkovq  30318  numclwwlk2lem1  30320  frgrregord013  30339  friendshipgt3  30342  ex-opab  30376  isgrpoi  30442  grpoidinv2  30459  hvsubeq0  31012  hvaddcan  31014  hvsubadd  31021  normsub0  31080  omlsi  31348  pjoml  31380  nonbooli  31595  pj11  31658  lnopeq  31953  nmopun  31958  pjclem4a  32142  pj3lem1  32150  strlem4  32198  hstrlem4  32206  jplem1  32212  superpos  32298  ifeqeqx  32486  disji2f  32521  disjif2  32525  disjabrex  32526  disjabrexf  32527  disjxpin  32532  disjunsn  32538  ofpreima  32608  fgreu  32615  fcnvgreu  32616  sgnsub  32782  gsumhashmul  33014  elrgspnlem2  33183  elrgspnlem3  33184  elrgspnlem4  33185  domnlcanOLD  33219  ismxidl  33399  xrge0iifcnv  33900  esumpr2  34034  eulerpartlemgvv  34344  eulerpartlemgh  34346  eulerpartlemgs2  34348  plymulx0  34515  lpadmax  34650  lpadright  34652  bnj1321  34994  f1resfz0f1d  35087  subfacp1lem3  35155  pconncn  35197  cnpconn  35203  txpconn  35205  connpconn  35208  cvmlift3lem2  35293  cvmlift3lem4  35295  cvmlift3  35301  snmlflim  35305  iota5f  35697  rankeq1o  36145  nn0prpw  36297  bj-csbsnlem  36877  bj-elgab  36913  bj-restsnss  37057  bj-restsnss2  37058  bj-imdirco  37164  wl-isseteq  37479  wl-ax12v2cl  37480  fin2so  37587  poimirlem2  37602  poimirlem18  37618  poimirlem21  37621  poimirlem25  37625  poimirlem26  37626  poimirlem27  37627  mblfinlem2  37638  mbfresfi  37646  cnambfre  37648  ftc1anclem8  37680  fdc  37725  istotbnd  37749  isexid2  37835  isgrpda  37935  ismaxidl  38020  mpobi123f  38142  mptbi12f  38146  disjressuc2  38360  qsdisjALTV  38592  parteq2  38753  lsatcmp  38982  lshpkrlem1  39089  trlval2  40142  cdlemg1cex  40567  cdlemm10N  41097  dicval  41155  lcmineqlem4  42005  grpods  42167  unitscyglem2  42169  unitscyglem3  42170  unitscyglem4  42171  exfinfldd  42176  nnn1suc  42239  resubval  42340  redivvald  42415  fsuppind  42563  unxpwdom3  43068  dgraalem  43118  dgraaub  43121  onsucf1lem  43242  frege104  43940  pm13.192  44383  2sbc6g  44388  2sbc5g  44389  pm14.122b  44396  equncomVD  44841  csbingVD  44857  csbsngVD  44866  csbxpgVD  44867  csbresgVD  44868  csbrngVD  44869  csbima12gALTVD  44870  csbunigVD  44871  csbfv12gALTVD  44872  relopabVD  44874  dvnprodlem1  45927  dvnprodlem2  45928  dvnprodlem3  45929  dvnprod  45930  fourierdlem42  46130  etransclem11  46226  etransclem12  46227  etransclem33  46248  nnfoctbdjlem  46436  hoimbl  46612  cfsetsnfsetf  47042  aiota0def  47080  euoreqb  47093  funressndmafv2rn  47207  funressnbrafv2  47228  dfatbrafv2b  47229  funbrafv2  47231  fnbrafv2b  47232  elsetpreimafvbi  47375  elsetpreimafveq  47381  imasetpreimafvbijlemfo  47389  fargshiftf1  47425  ichnreuop  47456  paireqne  47495  reupr  47506  isuspgrim0  47878  upgrimpths  47893  clnbgrgrim  47918  grimedg  47919  isubgr3stgrlem4  47953  isubgr3stgrlem7  47956  gpgedg2ov  48050  gpgedg2iv  48051  pgnbgreunbgrlem1  48097  pgnbgreunbgrlem2lem3  48100  pgnbgreunbgrlem4  48103  pgnbgreunbgr  48109  uspgrsprf1  48131  uspgrsprfo  48132  lidldomn1  48215  nn0sumshdiglem2  48607  mof0  48822  eufsnlem  48825  oppcmndclem  49002  isthincd2lem1  49410  termcbasmo  49468  termcarweu  49513  arweuthinc  49514  arweutermc  49515  setrec2lem2  49679