MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeq2 Unicode version

Theorem eqeq2 2472
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
StepHypRef Expression
1 id 22 . 2
21eqeq2d 2471 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395
This theorem is referenced by:  eqeq2i  2475  eqeq12  2476  eleq1OLD  2531  neeq2OLD  2741  alexeqg  3228  alexeq  3229  pm13.183  3240  eqeu  3270  moeq3  3276  mo2icl  3278  mob2  3279  euind  3286  reu6i  3290  reu2eqd  3296  reuind  3303  sbc2or  3336  sbc5  3352  csbiebg  3457  eqif  3979  sneq  4039  preqr1  4204  prel12  4207  preq12bg  4209  prel12g  4210  disji2  4439  disjprg  4448  dtruALT  4684  dtruALT2  4696  opth  4726  euotd  4753  solin  4828  ordequn  4983  ideqg  5159  resieq  5289  cnveqb  5467  cnveq0  5468  iota5  5576  funopg  5625  fneq2  5675  foeq3  5798  tz6.12f  5889  funbrfv  5911  fnbrfvb  5913  fvelimab  5929  elrnrexdm  6035  fconst5  6128  eufnfv  6146  f1veqaeq  6168  isosolem  6243  mpt2eq123  6356  ovmpt4g  6425  ov3  6439  ovg  6441  caovcang  6476  caovcan  6479  tfisi  6693  tfindsg  6695  findsg  6727  f1oweALT  6784  seqomlem2  7135  oawordeu  7223  omopth  7326  ereq2  7338  qsdisj  7407  eroveu  7425  2dom  7608  fundmen  7609  xpf1o  7699  nneneq  7720  cantnflem1  8129  cantnflem1OLD  8152  alephfp  8510  dfac5  8530  cardcf  8653  cfeq0  8657  sornom  8678  fpwwe2cbv  9029  fpwwe2lem3  9032  ltsosr  9492  map2psrpr  9508  axpre-lttri  9563  subval  9834  divval  10234  nn0ind-raph  10989  uzrdgfni  12069  sqeqor  12282  nn0opth2  12352  hashrabsn1  12442  elprchashprn2  12461  hashbclem  12501  hashbc  12502  hash2prde  12516  hash2pwpr  12519  wrdind  12702  wrd2ind  12703  reuccats1lem  12705  sqrtval  13070  sqrmo  13085  summolem2  13538  prodmolem2  13742  divides  13988  dvdstr  14018  odd2np1lem  14045  ndvdssub  14065  bitsinv1  14092  eucalglt  14214  ramcl2lem  14527  ramcl  14547  cshwrepswhash1  14587  imasaddfnlem  14925  posi  15579  sgrp2nmndlem3  16043  orbsta  16351  symgfvne  16413  symgfix2  16441  odlem1  16559  gexlem1  16599  slwispgp  16631  sylow3lem6  16652  efgrelexlemb  16768  gsumval3OLD  16908  gsumval3lem2  16910  pgpfac1  17131  pgpfaclem2  17133  pgpfac  17135  ablfaclem1  17136  isdomn  17943  mvrval  18077  coe1tmmul2  18317  coe1tmmul  18318  obsip  18752  uvcval  18816  mat1comp  18942  mat1dimid  18976  scmateALT  19014  marrepval  19064  marepvval  19069  minmar1val  19150  gsummatr01  19161  t0sep  19825  t1sep2  19870  is2ndc  19947  kqt0lem  20237  isr0  20238  isufil2  20409  xmeteq0  20841  imasf1oxmet  20878  xrsxmet  21314  iccpnfcnv  21444  dyadmax  22007  dyadmbl  22009  dvfsumle  22422  dvfsumabs  22424  dvfsumlem1  22427  mdegle0  22477  fta1g  22568  ig1peu  22572  fta1  22704  aalioulem2  22729  efopn  23039  efrlim  23299  musum  23467  dvdsmulf1o  23470  dchrsum2  23543  sumdchr2  23545  axtgcgrid  23860  axtgbtwnid  23863  tglowdim1i  23892  islmib  24153  axcontlem12  24278  wlkon  24533  wlkntrllem3  24563  spthonepeq  24589  fargshiftf1  24637  constr3trllem2  24651  wlklniswwlkn2  24700  usg2wlkeq  24708  wwlknredwwlkn  24726  wwlkextprop  24744  clwwlkn  24767  clwlkisclwwlklem2a4  24784  clwwlkext2edg  24802  clwwnisshclwwn  24809  hashecclwwlkn1  24834  usghashecclwwlk  24835  clwlkfoclwwlk  24845  2wlkonot  24865  2spthonot  24866  el2wlkonot  24869  el2spthonot  24870  el2spthonot0  24871  rusgraprop2  24942  rusgrasn  24945  rusgranumwlklem1  24949  rusgranumwlklem2  24950  rusgranumwlklem3  24951  rusgranumwlkg  24958  clwlknclwlkdifs  24960  frgra3vlem1  25000  3vfriswmgralem  25004  usg2spot2nb  25065  usgreg2spot  25067  2spotmdisj  25068  usgreghash2spot  25069  numclwwlkdisj  25080  numclwwlkovf  25081  numclwwlkovg  25087  numclwlk1lem2f1  25094  numclwwlkovq  25099  numclwwlkovh  25101  numclwwlk5  25112  frgrareg  25117  frgraregord013  25118  friendshipgt3  25121  ex-opab  25153  isgrpoi  25200  grpoidinv2  25220  isgrp2d  25237  isgrpda  25299  isexid2  25327  ghgrpOLD  25370  hvsubeq0  25985  hvaddcan  25987  hvsubadd  25994  normsub0  26053  omlsi  26322  pjoml  26354  nonbooli  26569  pj11  26632  lnopeq  26928  nmopun  26933  pjclem4a  27117  pj3lem1  27125  strlem4  27173  hstrlem4  27181  jplem1  27187  superpos  27273  rmoeq  27386  ifeqeqx  27419  disji2f  27438  disjif2  27442  disjabrex  27443  disjabrexf  27444  disjxpin  27447  disjunsn  27453  ofpreima  27507  fgreu  27513  fcnvgreu  27514  xrge0iifcnv  27915  esumpr2  28074  eulerpartlemgvv  28315  eulerpartlemgh  28317  eulerpartlemgs2  28319  sgnsub  28483  plymulx0  28504  subfacp1lem3  28626  pconcn  28669  cnpcon  28675  txpcon  28677  conpcon  28680  cvmlift3lem2  28765  cvmlift3lem4  28767  cvmlift3  28773  snmlflim  28777  ghomf1olem  29034  relexpindlem  29062  iota5f  29102  sltres  29424  nofulllem5  29466  rankeq1o  29828  fin2so  30040  mblfinlem2  30052  mbfresfi  30061  cnambfre  30063  ftc1anclem8  30097  nn0prpw  30141  f1opr  30215  fdc  30238  istotbnd  30265  ismaxidl  30437  mpt2bi123f  30571  mptbi12f  30575  unxpwdom3  31041  dgraalem  31094  dgraaub  31097  hashgcdeq  31158  pm13.192  31317  2sbc6g  31322  2sbc5g  31323  pm14.122b  31330  dvnprodlem1  31743  dvnprodlem2  31744  dvnprodlem3  31745  dvnprod  31746  fourierdlem42  31931  etransclem11  32028  etransclem12  32029  etransclem33  32050  fnhomeqhomf  32564  initoeu2lem1  32620  lidldomn1  32727  equncomVD  33668  csbingVD  33684  csbsngVD  33693  csbxpgVD  33694  csbresgVD  33695  csbrngVD  33696  csbima12gALTVD  33697  csbunigVD  33698  csbfv12gALTVD  33699  relopabVD  33701  bnj1321  34083  bj-csbsnlem  34470  lsatcmp  34728  lshpkrlem1  34835  trlval2  35888  cdlemg1cex  36314  cdlemm10N  36845  dicval  36903
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449
  Copyright terms: Public domain W3C validator