Theorem eqeq2 2775

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 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eqeq2d 2774	1 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  eqeq2i  2776  eqtr3  2785  clelab  2907  alexeqg  3610  pm13.183  3625  elab6g  3628  eqeu  3669  moeq3  3675  mo2icl  3677  mob2  3678  euind  3687  reu6i  3691  reu2eqd  3699  reuind  3716  sbc2or  3753  sbc5ALT  3773  csbiebg  3885  eqif  4529  sneq  4599  reusngf  4640  rexreusng  4645  reuprg0  4668  preq1b  4811  preq12bg  4818  preqsn  4827  disji2  5093  disjprg  5105  dtruALT  5359  opth  5458  euotd  5496  solin  5596  ideqg  5837  resieq  5989  cnveqb  6195  cnveq0  6196  reu3op  6293  reuop  6294  iota5  6519  funopg  6570  fneq2  6627  foeq3  6790  tz6.12f  6906  funbrfv  6929  fnbrfvb  6931  fvelimab  6953  elrnrexdm  7084  funsndifnop  7148  fconst5  7204  eufnfv  7227  f1veqaeq  7254  fpropnf1  7265  nf1const  7302  isosolem  7345  f1opr  7466  mpoeq123  7482  ovmpt4g  7557  ov3  7573  ovg  7575  caovcang  7611  caovcan  7614  tfisi  7851  tfindsg  7853  findsg  7890  f1oweALT  7965  seqomlem2  8434  oawordeu  8536  omopth  8644  ereq2  8699  qsdisj  8788  eroveu  8806  2dom  9023  fundmen  9024  xpf1o  9123  nneneq  9186  pwfir  9272  cantnflem1  9654  brttrcl  9678  ttrcltr  9681  ttrclss  9685  ttrclselem2  9691  updjud  9916  alephfp  10088  dfac5  10108  cardcf  10230  cfeq0  10235  sornom  10256  fpwwe2cbv  10610  fpwwe2lem3  10613  ltsosr  11074  map2psrpr  11090  axpre-lttri  11145  subval  11443  divval  11869  nn0ind-raph  12691  fvf1tp  13818  uzrdgfni  13990  sqeqor  14248  nn0opth2  14304  hashrabsn1  14406  elprchashprn2  14428  hashbclem  14485  hashbc  14486  hash2prde  14503  hash2pwpr  14509  brfi1indALT  14543  wrdind  14755  wrd2ind  14756  reuccatpfxs1lem  14779  cshf1  14843  wrdl3s3  14995  relexpindlem  15096  sgnsub  15139  sqrtval  15284  sqrmo  15298  reusq0  15512  summolem2  15763  prodmolem2  15985  divides  16307  dvdstr  16347  odd2np1lem  16393  ndvdssub  16462  bitsinv1  16495  eucalglt  16638  hashgcdeq  16844  ramcl2lem  17064  ramcl  17084  cshwrepswhash1  17157  imasaddfnlem  17577  fnhomeqhomf  17742  initoeu2lem1  18066  cat1lem  18148  posi  18368  sgrp2nmndlem3  18982  dfgrp2  19024  grpidinv  19060  dfgrp3lem  19099  orbsta  19378  symgfvne  19446  symgfix2  19481  odlem1  19600  gexlem1  19644  slwispgp  19676  sylow3lem6  19697  efgrelexlemb  19815  gsumval3lem2  19971  pgpfac1  20147  pgpfaclem2  20149  pgpfac  20151  ablfaclem1  20152  isdomn  20804  isdomn4  20814  domnlcanb  20818  domnrcanb  20820  obsip  21871  uvcval  21935  mvrval  22131  mhpval  22302  psdfval  22321  psdmvr  22332  coe1tmmul2  22437  coe1tmmul  22438  mat1comp  22597  mat1dimid  22631  scmateALT  22669  marrepval  22719  marepvval  22724  minmar1val  22805  gsummatr01  22816  t0sep  23481  t1sep2  23526  is2ndc  23603  kqt0lem  23893  isr0  23894  isufil2  24065  xmeteq0  24495  imasf1oxmet  24532  xrsxmet  24967  iccpnfcnv  25103  dyadmax  25757  dyadmbl  25759  dvfsumle  26180  dvfsumabs  26182  dvfsumlem1  26185  mdegle0  26234  fta1g  26327  ig1peu  26332  plyn0mulidp  26442  fta1  26469  aalioulem2  26496  taylthlem2  26537  efopn  26823  efrlim  27134  musum  27355  mpodvdsmulf1o  27358  dvdsmulf1o  27360  dchrsum2  27432  sumdchr2  27434  gausslemma2dlem0i  27528  addsqnreup  27607  2sqreulem1  27610  2sqreultblem  27612  2sqreunnlem1  27613  2sqreunnltblem  27615  2sqreulem3  27617  ltsres  27826  nosupprefixmo  27864  noinfprefixmo  27865  nosupcbv  27866  nosupno  27867  nosupfv  27870  noinfcbv  27881  noinfno  27882  noinffv  27885  elmade  28050  divsval  28382  noseqrdgfn  28499  bdayn0sf1o  28563  bdayfinbndlem2  28661  axtgcgrid  28732  axtgbtwnid  28735  tglowdim1i  28770  islmib  29096  prlngmo2  29206  axcontlem12  29325  upgredgpr  29492  ushgredgedg  29579  ushgredgedgloop  29581  rusgrpropnb  29933  rgrx0ndm  29943  uspgr2wlkeq  29995  wlkson  30004  upgrwlkdvdelem  30085  spthonepeq  30101  iswwlksnon  30202  wlklnwwlkln2lem  30231  wwlksnredwwlkn  30244  wwlksnextprop  30261  wwlksnwwlksnon  30264  elwwlks2ons3  30304  rusgrnumwwlklem  30322  clwlkclwwlklem2a4  30348  clwwlkn  30377  clwwlkext2edg  30407  hashecclwwlkn1  30428  umgrhashecclwwlk  30429  clwwlknon  30441  clwwlk0on0  30443  uhgr3cyclexlem  30532  1conngr  30545  frgr3vlem1  30624  3vfriswmgrlem  30628  frgrwopreglem3  30665  fusgreg2wsplem  30684  fusgreghash2wsp  30689  numclwlk1lem1  30720  numclwwlkovq  30725  numclwwlk2lem1  30727  frgrregord013  30746  friendshipgt3  30749  ex-opab  30783  isgrpoi  30850  grpoidinv2  30867  hvsubeq0  31420  hvaddcan  31422  hvsubadd  31429  normsub0  31488  omlsi  31756  pjoml  31788  nonbooli  32003  pj11  32066  lnopeq  32361  nmopun  32366  pjclem4a  32550  pj3lem1  32558  strlem4  32606  hstrlem4  32614  jplem1  32620  superpos  32706  ifeqeqx  32888  disji2f  32922  disjif2  32926  disjabrex  32927  disjabrexf  32928  disjxpin  32933  disjunsn  32939  ofpreima  33010  fgreu  33016  fcnvgreu  33017  gsumhashmul  33387  elrgspnlem2  33563  elrgspnlem3  33564  elrgspnlem4  33565  ismxidl  33745  mplasclco  33906  mplmulmvr  33929  psrmonmul2  33941  esplyfval  33953  esplyfval0  33954  esplyfv  33960  esplyfval3  33962  esplyfvaln  33964  xrge0iifcnv  34323  esumpr2  34457  eulerpartlemgvv  34766  eulerpartlemgh  34768  eulerpartlemgs2  34770  lpadmax  35072  lpadright  35074  bnj1321  35415  f1resfz0f1d  35605  subfacp1lem3  35674  pconncn  35716  cnpconn  35722  txpconn  35724  connpconn  35727  cvmlift3lem2  35812  cvmlift3lem4  35814  cvmlift3  35820  snmlflim  35824  iota5f  36216  rankeq1o  36663  nn0prpw  36834  tr0elw  36995  tr0el  36996  dfttc4lem1  37039  elttcirr  37042  bj-csbsnlem  37538  bj-elgab  37575  bj-restsnss  37725  bj-restsnss2  37726  bj-imdirco  37834  wl-isseteq  38151  wl-ax12v2cl  38152  wl-dfcleq  38160  fin2so  38258  poimirlem2  38273  poimirlem18  38289  poimirlem21  38292  poimirlem25  38296  poimirlem26  38297  poimirlem27  38298  mblfinlem2  38309  mbfresfi  38317  cnambfre  38319  ftc1anclem8  38351  fdc  38396  istotbnd  38420  isexid2  38506  isgrpda  38606  ismaxidl  38691  mpobi123f  38811  mptbi12f  38815  disjressuc2  39060  qsdisjALTV  39348  parteq2  39527  lsatcmp  39777  lshpkrlem1  39884  trlval2  40937  cdlemg1cex  41362  cdlemm10N  41892  dicval  41950  lcmineqlem4  42799  grpods  42961  unitscyglem2  42963  unitscyglem3  42964  unitscyglem4  42965  exfinfldd  42970  nnn1suc  43033  resubval  43128  redivvald  43203  fsuppind  43322  unxpwdom3  43822  dgraalem  43872  dgraaub  43875  onsucf1lem  43996  frege104  44693  pm13.192  45120  2sbc6g  45125  2sbc5g  45126  pm14.122b  45133  equncomVD  45576  csbingVD  45592  csbsngVD  45601  csbxpgVD  45602  csbresgVD  45603  csbrngVD  45604  csbima12gALTVD  45605  csbunigVD  45606  csbfv12gALTVD  45607  relopabVD  45609  dvnprodlem1  46660  dvnprodlem2  46661  dvnprodlem3  46662  dvnprod  46663  fourierdlem42  46863  etransclem11  46959  etransclem12  46960  etransclem33  46981  nnfoctbdjlem  47169  hoimbl  47345  cfsetsnfsetf  47795  aiota0def  47833  euoreqb  47846  funressndmafv2rn  47960  funressnbrafv2  47981  dfatbrafv2b  47982  funbrafv2  47984  fnbrafv2b  47985  elsetpreimafvbi  48140  elsetpreimafveq  48146  imasetpreimafvbijlemfo  48154  fargshiftf1  48190  ichnreuop  48221  paireqne  48260  reupr  48271  isuspgrim0  48659  upgrimpths  48674  clnbgrgrim  48699  grimedg  48700  isubgr3stgrlem4  48734  isubgr3stgrlem7  48737  gpgedg2ov  48831  gpgedg2iv  48832  pgnbgreunbgrlem1  48878  pgnbgreunbgrlem2lem3  48881  pgnbgreunbgrlem4  48884  pgnbgreunbgr  48890  uspgrsprf1  48912  uspgrsprfo  48913  lidldomn1  48996  nn0sumshdiglem2  49402  mof0  49616  eufsnlem  49619  oppcmndclem  49795  isthincd2lem1  50203  termcbasmo  50261  termcarweu  50306  arweuthinc  50307  arweutermc  50308  setrec2lem2  50472