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

Theorem elsn 4043
Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
elsn
Distinct variable group:   ,

Proof of Theorem elsn
StepHypRef Expression
1 df-sn 4030 . 2
21abeq2i 2584 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  =wceq 1395  e.wcel 1818  {csn 4029
This theorem is referenced by:  dfpr2  4044  ralsnsg  4061  rexsns  4062  rexsnsOLD  4063  disjsn  4090  snprc  4093  euabsn2  4101  snss  4154  raldifsnb  4161  difprsnss  4165  pwpw0  4178  eqsn  4191  snsspw  4201  pwsnALT  4244  dfnfc2  4267  uni0b  4274  uni0c  4275  sndisj  4444  reusv6OLD  4663  rext  4700  moabex  4711  exss  4715  otiunsndisj  4758  fconstmpt  5048  opeliunxp  5056  restidsing  5335  xpdifid  5440  dmsnopg  5484  dfmpt3  5708  nfunsn  5902  dffv2  5946  fsn  6069  fnasrn  6077  fnsnb  6090  fmptsng  6092  fmptsnd  6093  fconstfvOLD  6134  fvclss  6154  eusvobj2  6289  suceloni  6648  opabex3d  6778  opabex3  6779  oarec  7230  ixp0x  7517  xpsnen  7621  marypha2lem2  7916  elirrv  8044  sucprcregOLD  8047  cantnfp1lem1  8118  cantnfp1lem3  8120  cantnfp1lem1OLD  8144  cantnfp1lem3OLD  8146  dfac5lem1  8525  dfac5lem2  8526  dfac5lem4  8528  fin1a2lem11  8811  axdc4lem  8856  axcclem  8858  xrsupexmnf  11525  xrinfmexpnf  11526  iccid  11603  fzsn  11754  fzpr  11764  seqz  12155  hashf1  12506  pr2pwpr  12520  fsum2dlem  13585  incexc2  13650  prodsn  13767  fprod2dlem  13784  ef0lem  13814  divalgmod  14064  1nprm  14222  isprm2lem  14224  vdwapun  14492  cshwsiun  14584  xpsc0  14957  xpsc1  14958  mgmidsssn0  15896  mnd1id  15963  symg1bas  16421  pmtrprfvalrn  16513  gex1  16611  sylow2alem1  16637  lsmdisj2  16700  0frgp  16797  0cyg  16895  prmcyg  16896  dprddisj2  17087  dprddisj2OLD  17088  ablfacrp  17117  kerf1hrm  17392  lspdisj  17771  lidlnz  17876  psrlidm  18056  psrlidmOLD  18057  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  evlslem1  18184  mulgrhm2  18533  mulgrhm2OLD  18536  ocvin  18705  maducoeval2  19142  madugsum  19145  en2top  19487  restsn  19671  ist1-3  19850  ordtt1  19880  cmpcld  19902  unisngl  20028  dissnlocfin  20030  ptopn2  20085  snfil  20365  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALTlem4  20550  haustsms2  20635  tsmsxplem1  20655  tsmsxplem2  20656  ust0  20722  dscopn  21094  nmoid  21249  limcdif  22280  ellimc2  22281  limcmpt  22287  limcres  22290  ply1remlem  22563  plyeq0lem  22607  plyremlem  22700  aaliou2  22736  radcnv0  22811  abelthlem2  22827  wilthlem2  23343  vmappw  23390  ppinprm  23426  chtnprm  23428  musumsum  23468  dchrhash  23546  lgsquadlem1  23629  lgsquadlem2  23630  isusgra0  24347  usgraop  24350  nbcusgra  24463  usgrasscusgra  24483  rusgranumwlkb0  24953  frgrancvvdeqlem9  25041  frgrawopreglem4  25047  usg2spot2nb  25065  grposn  25217  ablosn  25349  hsn0elch  26166  xrge0iifiso  27917  qqhval2  27963  esumnul  28059  esumfzf  28075  sibfof  28282  plymulx0  28504  signstf0  28525  signstfvneq0  28529  sconpi1  28684  ghomsn  29028  dffr5  29182  elima4  29209  wfrlem14  29356  wfrlem15  29357  brsingle  29567  dfiota3  29573  funpartfun  29593  dfrdg4  29600  0idl  30422  smprngopr  30449  isdmn3  30471  pellexlem5  30769  jm2.23  30938  flcidc  31123  iccintsng  31563  icoiccdif  31564  prodsnf  31587  limcrecl  31635  lptioo2  31637  lptioo1  31638  limcresiooub  31648  limcresioolb  31649  icccncfext  31690  dvmptfprodlem  31741  dvnprodlem3  31745  dirkercncflem2  31886  fourierdlem40  31929  fourierdlem48  31937  fourierdlem51  31940  fourierdlem62  31951  fourierdlem66  31955  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem78  31967  fourierdlem79  31968  fourierdlem93  31982  fourierdlem101  31990  fourierdlem103  31992  fourierdlem104  31993  fouriersw  32014  elaa2  32017  etransclem44  32061  etransc  32066  funressnfv  32213  dfdfat2  32216  tz6.12-afv  32258  otiunsndisjX  32301  xpsnopab  32453  opeliun2xp  32922  aacllem  33216  snssiALTVD  33627  snssiALT  33628  bnj145OLD  33782  bnj521  33792  bj-csbsnlem  34470  lshpdisj  34712  lsat0cv  34758  snatpsubN  35474  dibelval3  36874  dib1dim  36892  dvh2dim  37172  mapd0  37392  hdmap14lem13  37610  snhesn  37809
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-5 1704  ax-6 1747  ax-7 1790  ax-12 1854  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-sn 4030
  Copyright terms: Public domain W3C validator