Theorem eqeq2 2781

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  eqeq2i  2782  eqtr3  2791  clelab  2913  alexeqg  3619  pm13.183  3634  elab6g  3637  eqeu  3678  moeq3  3684  mo2icl  3686  mob2  3687  euind  3696  reu6i  3700  reu2eqd  3708  reuind  3725  sbc2or  3762  sbc5ALT  3782  csbiebg  3893  eqif  4534  sneq  4604  reusngf  4645  rexreusng  4650  reuprg0  4673  preq1b  4815  preq12bg  4822  preqsn  4831  disji2  5097  disjprg  5109  dtruALT  5360  opth  5459  euotd  5497  solin  5597  ideqg  5838  resieq  5990  cnveqb  6196  cnveq0  6197  reu3op  6294  reuop  6295  iota5  6520  funopg  6571  fneq2  6628  foeq3  6791  tz6.12f  6907  funbrfv  6930  fnbrfvb  6932  fvelimab  6954  elrnrexdm  7085  funsndifnop  7149  fconst5  7205  eufnfv  7228  f1veqaeq  7255  fpropnf1  7266  nf1const  7303  isosolem  7346  f1opr  7467  mpoeq123  7483  ovmpt4g  7558  ov3  7574  ovg  7576  caovcang  7612  caovcan  7615  tfisi  7854  tfindsg  7856  findsg  7893  f1oweALT  7968  seqomlem2  8437  oawordeu  8539  omopth  8647  ereq2  8702  qsdisj  8791  eroveu  8809  2dom  9026  fundmen  9027  xpf1o  9126  nneneq  9189  pwfir  9275  cantnflem1  9657  brttrcl  9681  ttrcltr  9684  ttrclss  9688  ttrclselem2  9694  updjud  9919  alephfp  10091  dfac5  10111  cardcf  10234  cfeq0  10239  sornom  10260  fpwwe2cbv  10614  fpwwe2lem3  10617  ltsosr  11078  map2psrpr  11094  axpre-lttri  11149  subval  11447  divval  11873  nn0ind-raph  12695  fvf1tp  13821  uzrdgfni  13993  sqeqor  14251  nn0opth2  14307  hashrabsn1  14409  elprchashprn2  14431  hashbclem  14488  hashbc  14489  hash2prde  14506  hash2pwpr  14512  brfi1indALT  14546  wrdind  14758  wrd2ind  14759  reuccatpfxs1lem  14782  cshf1  14846  wrdl3s3  14998  relexpindlem  15099  sgnsub  15142  sqrtval  15287  sqrmo  15301  reusq0  15515  summolem2  15766  prodmolem2  15988  divides  16311  dvdstr  16351  odd2np1lem  16397  ndvdssub  16466  bitsinv1  16499  eucalglt  16642  hashgcdeq  16848  ramcl2lem  17068  ramcl  17088  cshwrepswhash1  17161  imasaddfnlem  17581  fnhomeqhomf  17746  initoeu2lem1  18070  cat1lem  18152  posi  18372  sgrp2nmndlem3  18986  dfgrp2  19028  grpidinv  19064  dfgrp3lem  19103  orbsta  19382  symgfvne  19450  symgfix2  19485  odlem1  19604  gexlem1  19648  slwispgp  19680  sylow3lem6  19701  efgrelexlemb  19819  gsumval3lem2  19975  pgpfac1  20151  pgpfaclem2  20153  pgpfac  20155  ablfaclem1  20156  isdomn  20789  isdomn4  20799  domnlcanb  20803  domnrcanb  20805  obsip  21839  uvcval  21903  mvrval  22099  mhpval  22270  psdfval  22289  psdmvr  22300  coe1tmmul2  22405  coe1tmmul  22406  mat1comp  22565  mat1dimid  22599  scmateALT  22637  marrepval  22687  marepvval  22692  minmar1val  22773  gsummatr01  22784  t0sep  23449  t1sep2  23494  is2ndc  23571  kqt0lem  23861  isr0  23862  isufil2  24033  xmeteq0  24463  imasf1oxmet  24500  xrsxmet  24935  iccpnfcnv  25071  dyadmax  25725  dyadmbl  25727  dvfsumle  26148  dvfsumabs  26150  dvfsumlem1  26153  mdegle0  26202  fta1g  26295  ig1peu  26300  plyn0mulidp  26410  fta1  26437  aalioulem2  26462  taylthlem2  26502  efopn  26788  efrlim  27099  musum  27320  mpodvdsmulf1o  27323  dvdsmulf1o  27325  dchrsum2  27397  sumdchr2  27399  gausslemma2dlem0i  27493  addsqnreup  27572  2sqreulem1  27575  2sqreultblem  27577  2sqreunnlem1  27578  2sqreunnltblem  27580  2sqreulem3  27582  ltsres  27791  nosupprefixmo  27829  noinfprefixmo  27830  nosupcbv  27831  nosupno  27832  nosupfv  27835  noinfcbv  27846  noinfno  27847  noinffv  27850  elmade  28015  divsval  28347  noseqrdgfn  28464  bdayn0sf1o  28528  bdayfinbndlem2  28626  axtgcgrid  28697  axtgbtwnid  28700  tglowdim1i  28735  islmib  29053  axcontlem12  29265  upgredgpr  29432  ushgredgedg  29519  ushgredgedgloop  29521  rusgrpropnb  29873  rgrx0ndm  29883  uspgr2wlkeq  29935  wlkson  29944  upgrwlkdvdelem  30025  spthonepeq  30041  iswwlksnon  30142  wlklnwwlkln2lem  30171  wwlksnredwwlkn  30184  wwlksnextprop  30201  wwlksnwwlksnon  30204  elwwlks2ons3  30244  rusgrnumwwlklem  30262  clwlkclwwlklem2a4  30288  clwwlkn  30317  clwwlkext2edg  30347  hashecclwwlkn1  30368  umgrhashecclwwlk  30369  clwwlknon  30381  clwwlk0on0  30383  uhgr3cyclexlem  30472  1conngr  30485  frgr3vlem1  30564  3vfriswmgrlem  30568  frgrwopreglem3  30605  fusgreg2wsplem  30624  fusgreghash2wsp  30629  numclwlk1lem1  30660  numclwwlkovq  30665  numclwwlk2lem1  30667  frgrregord013  30686  friendshipgt3  30689  ex-opab  30723  isgrpoi  30790  grpoidinv2  30807  hvsubeq0  31360  hvaddcan  31362  hvsubadd  31369  normsub0  31428  omlsi  31696  pjoml  31728  nonbooli  31943  pj11  32006  lnopeq  32301  nmopun  32306  pjclem4a  32490  pj3lem1  32498  strlem4  32546  hstrlem4  32554  jplem1  32560  superpos  32646  ifeqeqx  32828  disji2f  32862  disjif2  32866  disjabrex  32867  disjabrexf  32868  disjxpin  32873  disjunsn  32879  ofpreima  32950  fgreu  32956  fcnvgreu  32957  gsumhashmul  33327  elrgspnlem2  33503  elrgspnlem3  33504  elrgspnlem4  33505  ismxidl  33689  mplasclco  33850  mplmulmvr  33873  psrmonmul2  33885  esplyfval  33897  esplyfval0  33898  esplyfv  33904  esplyfval3  33906  esplyfvaln  33908  xrge0iifcnv  34267  esumpr2  34401  eulerpartlemgvv  34710  eulerpartlemgh  34712  eulerpartlemgs2  34714  lpadmax  35016  lpadright  35018  bnj1321  35359  f1resfz0f1d  35503  subfacp1lem3  35572  pconncn  35614  cnpconn  35620  txpconn  35622  connpconn  35625  cvmlift3lem2  35710  cvmlift3lem4  35712  cvmlift3  35718  snmlflim  35722  iota5f  36114  rankeq1o  36561  nn0prpw  36722  tr0elw  36883  tr0el  36884  dfttc4lem1  36927  elttcirr  36930  bj-csbsnlem  37426  bj-elgab  37462  bj-restsnss  37612  bj-restsnss2  37613  bj-imdirco  37721  wl-isseteq  38038  wl-ax12v2cl  38039  wl-dfcleq  38047  fin2so  38145  poimirlem2  38160  poimirlem18  38176  poimirlem21  38179  poimirlem25  38183  poimirlem26  38184  poimirlem27  38185  mblfinlem2  38196  mbfresfi  38204  cnambfre  38206  ftc1anclem8  38238  fdc  38283  istotbnd  38307  isexid2  38393  isgrpda  38493  ismaxidl  38578  mpobi123f  38700  mptbi12f  38704  disjressuc2  38949  qsdisjALTV  39237  parteq2  39416  lsatcmp  39666  lshpkrlem1  39773  trlval2  40826  cdlemg1cex  41251  cdlemm10N  41781  dicval  41839  lcmineqlem4  42688  grpods  42850  unitscyglem2  42852  unitscyglem3  42853  unitscyglem4  42854  exfinfldd  42859  nnn1suc  42922  resubval  43017  redivvald  43092  fsuppind  43213  unxpwdom3  43713  dgraalem  43763  dgraaub  43766  onsucf1lem  43887  frege104  44584  pm13.192  45011  2sbc6g  45016  2sbc5g  45017  pm14.122b  45024  equncomVD  45467  csbingVD  45483  csbsngVD  45492  csbxpgVD  45493  csbresgVD  45494  csbrngVD  45495  csbima12gALTVD  45496  csbunigVD  45497  csbfv12gALTVD  45498  relopabVD  45500  dvnprodlem1  46551  dvnprodlem2  46552  dvnprodlem3  46553  dvnprod  46554  fourierdlem42  46754  etransclem11  46850  etransclem12  46851  etransclem33  46872  nnfoctbdjlem  47060  hoimbl  47236  cfsetsnfsetf  47683  aiota0def  47721  euoreqb  47734  funressndmafv2rn  47848  funressnbrafv2  47869  dfatbrafv2b  47870  funbrafv2  47872  fnbrafv2b  47873  elsetpreimafvbi  48028  elsetpreimafveq  48034  imasetpreimafvbijlemfo  48042  fargshiftf1  48078  ichnreuop  48109  paireqne  48148  reupr  48159  isuspgrim0  48547  upgrimpths  48562  clnbgrgrim  48587  grimedg  48588  isubgr3stgrlem4  48622  isubgr3stgrlem7  48625  gpgedg2ov  48719  gpgedg2iv  48720  pgnbgreunbgrlem1  48766  pgnbgreunbgrlem2lem3  48769  pgnbgreunbgrlem4  48772  pgnbgreunbgr  48778  uspgrsprf1  48800  uspgrsprfo  48801  lidldomn1  48884  nn0sumshdiglem2  49286  mof0  49500  eufsnlem  49503  oppcmndclem  49679  isthincd2lem1  50087  termcbasmo  50145  termcarweu  50190  arweuthinc  50191  arweutermc  50192  setrec2lem2  50356