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

Theorem eleq2 2530
Description: Equality implies equivalence of membership. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)
Assertion
Ref Expression
eleq2

Proof of Theorem eleq2
StepHypRef Expression
1 id 22 . 2
21eleq2d 2527 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818
This theorem is referenced by:  eleq12  2533  eleq2i  2535  eleq2dOLD  2538  nelneq2  2575  dvelimdc  2642  nelne1  2786  neleq2OLD  2798  raleqf  3050  rexeqf  3051  reueq1f  3052  rmoeq1f  3053  rabeqf  3102  clel3g  3237  clel4  3239  sbcbi2  3378  sbcel2gv  3394  csbeq2  3438  difeq2  3615  uneq1  3650  ineq1  3692  unineq  3747  n0i  3789  sbnfc2  3854  disjel  3873  elif  3981  exsnrex  4067  sneqr  4197  preqr1  4204  preq12b  4206  prel12  4207  elunii  4254  eluniab  4260  ssuni  4271  elinti  4295  elintab  4297  intss1  4301  intmin  4306  intab  4317  iineq2  4348  dfiin2g  4363  breq  4454  zfrepclf  4569  axsep2  4574  zfauscl  4575  sseliALT  4583  inuni  4614  pwne0  4622  elALT  4695  rext  4700  intid  4710  opth1  4725  opthwiener  4754  ordtri1  4916  ordtri3  4919  nsuceq0  4963  suctr  4966  ordnbtwn  4973  xpeq1  5018  xpeq2  5019  opthprc  5052  funopg  5625  dffv2  5946  fveqdmss  6026  dffo4  6047  fnsnb  6090  elunirn  6163  f1oiso  6247  canth  6254  eusvobj2  6289  mpt2eq123  6356  ndmovg  6458  snnex  6606  uniuni  6609  iunpw  6614  oneqmin  6640  onuninsuci  6675  nlimsucg  6677  limomss  6705  nnlim  6713  peano5  6723  unielxp  6836  cnvf1o  6899  smoel  7050  smo11  7054  tz7.44-2  7092  oawordeulem  7222  oaordex  7226  omordi  7234  oneo  7249  oeordi  7255  oeoa  7265  oeoe  7267  nnmordi  7299  nnaordex  7306  omabs  7315  nnneo  7319  omsmolem  7321  elqsn0  7399  qsel  7409  mapsn  7480  undifixp  7525  boxriin  7531  boxcutc  7532  fineqvlem  7754  fineqv  7755  pssnn  7758  fissuni  7845  dffi2  7903  inficl  7905  dffi3  7911  wofib  7991  zfregcl  8041  en3lplem1  8052  en3lp  8054  suc11reg  8057  inf0  8059  inf3lem2  8067  inf3lem3  8068  infeq5i  8074  axinf2  8078  dfom3  8085  elom3  8086  noinfepOLD  8098  cantnfle  8111  oemapvali  8124  cantnflem1c  8127  cantnflem1  8129  cantnfleOLD  8141  cantnflem1cOLD  8150  cantnflem1OLD  8152  tc2  8194  r1sdom  8213  rankwflemb  8232  rankval3b  8265  rankunb  8289  rankuni2b  8292  tcrank  8323  cardlim  8374  cardprclem  8381  infxpenlem  8412  alephnbtwn  8473  alephordi  8476  cardaleph  8491  alephfp  8510  alephval3  8512  aceq1  8519  aceq2  8521  dfac3  8523  dfac5lem2  8526  dfac5lem4  8528  dfac2  8532  kmlem2  8552  kmlem4  8554  coflim  8662  cfsmolem  8671  fin23lem30  8743  isf32lem2  8755  isf34lem4  8778  axdc2lem  8849  axdc3lem2  8852  axdc3lem4  8854  axdc4lem  8856  zorn2lem7  8903  axdclem  8920  brdom7disj  8930  brdom6disj  8931  axpowndlem3  8996  axpowndlem3OLD  8997  winainflem  9092  iswun  9103  eltskg  9149  inar1  9174  elgrug  9191  inaprc  9235  eltskm  9242  addnidpi  9300  indpi  9306  nqereu  9328  elnp  9386  elnpi  9387  genpnnp  9404  ltaddpr  9433  dfnn2  10574  dfnn3  10575  dfuzi  10978  uz11  11132  elfzonlteqm1  11891  om2uzlti  12061  axdc4uz  12093  hashrabsn1  12442  hashbclem  12501  hashf1lem2  12505  hash2prd  12518  hash2prv  12525  wrdsymb0  12575  lsw0  12586  prodeq1f  13715  rpnnen2lem1  13948  rpnnen2lem2  13949  sadcp1  14105  ismre  14987  isacs  15048  clatl  15746  mreclatBAD  15817  issubm  15978  cycsubg  16229  isnsg  16230  subgacs  16236  nsgacs  16237  resghm  16283  ghmeql  16289  gsmsymgreq  16457  f1otrspeq  16472  pmtrval  16476  pmtrdifellem4  16504  pmtrprfval  16512  gsumzsplit  16944  gsumzsplitOLD  16945  pgpfac1lem1  17125  pgpfac1lem5  17130  pgpfac1  17131  issubrg  17429  islss  17581  lssacs  17613  lspsneq0  17658  lmhmeql  17701  lspdisjb  17772  lidl1el  17866  lidldvgen  17903  0ring01eq  17919  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  islindf4  18873  m1detdiag  19099  mdetunilem9  19122  maducoeval2  19142  madugsum  19145  chpmat1dlem  19336  istopg  19404  fiinbas  19453  topbas  19474  ppttop  19508  pptbas  19509  epttop  19510  elcls  19574  clsndisj  19576  elcls3  19584  iscldtop  19596  neiptopnei  19633  restbas  19659  restntr  19683  pnfnei  19721  mnfnei  19722  cnpimaex  19757  lmcvg  19763  iscnp4  19764  cncnpi  19779  cnconst2  19784  cnprest  19790  cnprest2  19791  cnpdis  19794  lmss  19799  lmff  19802  cnt0  19847  ist1-3  19850  cnhaus  19855  isreg2  19878  dishaus  19883  ordthauslem  19884  cmpsublem  19899  cmpsub  19900  cmpcld  19902  hauscmplem  19906  bwthOLD  19911  uncon  19930  concompid  19932  concompcon  19933  concompss  19934  1stcfb  19946  1stcrest  19954  2ndcctbss  19956  2ndcomap  19959  dis2ndc  19961  1stcelcls  19962  llyeq  19971  nllyeq  19972  restnlly  19983  restlly  19984  islly2  19985  lly1stc  19997  dislly  19998  hauspwdom  20002  finlocfin  20021  unisngl  20028  dissnlocfin  20030  locfindis  20031  comppfsc  20033  llycmpkgen2  20051  txbas  20068  eltx  20069  ptpjopn  20113  ptclsg  20116  dfac14lem  20118  txcnp  20121  ptcnplem  20122  ptcnp  20123  txlly  20137  pthaus  20139  txtube  20141  txhaus  20148  txlm  20149  tx1stc  20151  txkgen  20153  xkohaus  20154  xkopt  20156  xkococnlem  20160  tgqtop  20213  kqfvima  20231  kqt0lem  20237  isr0  20238  r0cld  20239  regr1lem  20240  kqreglem1  20242  kqreglem2  20243  reghmph  20294  fbssfi  20338  isfil  20348  filuni  20386  isufil  20404  isufil2  20409  uffix  20422  fixufil  20423  uffixfr  20424  uffixsn  20426  rnelfm  20454  flimopn  20476  flimrest  20484  flimcls  20486  flftg  20497  txflf  20507  fclsopni  20516  fclsrest  20525  fclscf  20526  fcfnei  20536  alexsublem  20544  alexsubALTlem3  20549  alexsubALT  20551  tmdgsum2  20595  symgtgp  20600  subgntr  20605  opnsubg  20606  tgpconcompeqg  20610  ghmcnp  20613  tgpt0  20617  qustgpopn  20618  tsmsi  20632  tsmssubm  20644  tsmssplit  20654  isust  20706  ustn0  20723  blssps  20927  blss  20928  blssexps  20929  blssex  20930  neibl  21004  blcld  21008  metss  21011  methaus  21023  met1stc  21024  met2ndci  21025  metrest  21027  prdsxmslem2  21032  metcnp3  21043  dscopn  21094  idnghm  21250  qdensere  21277  tgioo  21301  tgqioo  21305  zdis  21321  xrge0tsms  21339  cnheibor  21455  lmmbr  21697  bcthlem4  21766  ovolicc2lem5  21932  dyadmbllem  22008  i1fd  22088  itg11  22098  itg2gt0  22167  itgeq1f  22178  bddmulibl  22245  ellimc2  22281  limcnlp  22282  ellimc3  22283  limcflf  22285  limciun  22298  lhop1lem  22414  ig1pdvds  22577  plycpn  22685  aannenlem2  22725  efopn  23039  xrlimcnp  23298  wilthlem2  23343  wilthlem3  23344  wilth  23345  tghilbert1_1  24017  tghilbert1_2  24018  colline  24030  lmif  24151  islmib  24153  usgra2edg  24382  usgraedg4  24387  nbgraf1olem1  24441  nbgraf1olem3  24443  nb3graprlem1  24451  nb3graprlem2  24452  uvtx01vtx  24492  uvtxnbgravtx  24495  2trllemF  24551  wlkntrl  24564  constr1trl  24590  eleclclwwlkn  24833  vdgr1a  24906  vdusgra0nedg  24908  usgravd0nedg  24918  eupath2lem1  24977  vdn0frgrav2  25023  vdgn0frgrav2  25024  frgrancvvdeqlem4  25033  frgrancvvdeqlem7  25036  frgrancvvdeqlemA  25037  frgrancvvdeqlemC  25039  frgrawopreg1  25050  frgrawopreg2  25051  lpni  25181  rngoueqz  25432  issh  26125  pjoc1  26352  h1dn0  26470  spansneleqi  26487  nonbooli  26569  pjch  26612  pjnel  26644  cdjreui  27351  rexunirn  27390  rabsnel  27402  opabdm  27464  opabrn  27465  fpwrelmapffslem  27555  fpwrelmap  27556  xrge0tsmsd  27775  reff  27842  tpr2rico  27894  lmxrge0  27934  indval  28027  issiga  28111  isrnsigaOLD  28112  isrnsiga  28113  ddeval1  28206  ddeval0  28207  ddemeas  28208  ismbfm  28223  isanmbfm  28227  dya2icoseg  28248  dya2iocnrect  28252  ballotlem7  28474  erdszelem1  28635  kur14lem9  28658  cnllyscon  28690  cvmcov  28708  cvmsss2  28719  cvmcov2  28720  cvmseu  28721  cvmsiota  28722  cvmopnlem  28723  cvmliftlem15  28743  mclsssvlem  28922  mclsind  28930  rtrclreclem.trans  29069  untelirr  29080  untsucf  29082  dfon2lem4  29218  dfon2lem7  29221  dfon2lem9  29223  soseq  29334  frrlem4  29390  frrlem5e  29395  frrlem11  29399  nodenselem8  29448  nocvxminlem  29450  nofulllem5  29466  dfiota3  29573  funpartlem  29592  funpartfun  29593  tfrqfree  29601  linethru  29803  hilbert1.1  29804  hilbert1.2  29805  rankelg  29825  elhf2  29832  fin2so  30040  heicant  30049  mblfinlem1  30051  ftc1anc  30098  ftc2nc  30099  fneint  30166  neibastop2lem  30178  cover2  30204  isbnd2  30279  prdstotbnd  30290  heibor1lem  30305  grpokerinj  30347  isidl  30411  1idl  30423  0rngo  30424  ispridl  30431  smprngopr  30449  isfldidl  30465  isdmn3  30471  mpt2bi123f  30571  iineq12f  30573  mptbi12f  30575  elmzpcl  30658  diophren  30747  dford3lem2  30969  ttac  30978  pw2f1ocnv  30979  wepwsolem  30987  kelac1  31009  sdrgacs  31150  expgrowthi  31238  dvconstbi  31239  elunif  31391  fnchoice  31404  icccncfext  31690  stoweidlem27  31809  stoweidlem35  31817  stoweidlem46  31828  stoweidlem52  31834  funressnfv  32213  fnbrafvb  32239  afvco2  32261  ndmaovg  32269  aovmpt4g  32286  fzoopth  32340  usgpredgv  32399  usgvincvad  32404  usgvincvadALT  32407  usgvad2edg  32411  usg2edgneu  32412  usgedgvadf1lem1  32413  usgedgvadf1lem2  32414  usgedgvadf1ALTlem1  32416  usgedgvadf1ALTlem2  32417  usgedgleord  32419  usgedgleordALT  32420  issubmgm  32477  initoid  32611  termoid  32612  initoeu2lem1  32620  c0snmgmhm  32720  c0snmhm  32721  rngccatidOLD  32797  ringccatidOLD  32860  ldepspr  33074  tratrb  33307  suctrALT2VD  33636  suctrALT2  33637  en3lplem1VD  33643  en3lpVD  33645  tratrbVD  33661  suctrALTcf  33722  suctrALTcfVD  33723  suctrALT3  33724  unisnALT  33726  bnj145OLD  33782  bnj216  33787  bnj563  33800  bnj956  33835  bnj545  33953  bnj548  33955  bnj570  33963  bnj900  33987  bnj929  33994  bnj964  34001  bnj983  34009  bnj1001  34016  bnj1145  34049  bnj1398  34090  bnj1498  34117  bj-rabeqd  34488  bj-cleq  34519  bj-snsetex  34521  bj-nuliota  34586  bj-elopg  34602  lsateln0  34720  ispsubsp  35469  linepsubN  35476  elpcliN  35617  dvh3dim3N  37176  dochsnnz  37177  mapdindp3  37449
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-an 371  df-ex 1613  df-cleq 2449  df-clel 2452
  Copyright terms: Public domain W3C validator