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

Theorem elsni 4054
Description: There is only one element in a singleton. (Contributed by NM, 5-Jun-1994.)
Assertion
Ref Expression
elsni

Proof of Theorem elsni
StepHypRef Expression
1 elsncg 4052 . 2
21ibi 241 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  {csn 4029
This theorem is referenced by:  elsnc2g  4059  elpwunsn  4070  disjsn2  4091  rabsnifsb  4098  sssn  4188  disjxsn  4446  opth1  4725  elsuci  4949  sosn  5074  ressn  5548  funcnvsn  5638  fvconst  6089  fnsnb  6090  fmptap  6094  fvunsn  6103  mpt2snif  6396  1stconst  6888  2ndconst  6889  reldmtpos  6982  tpostpos  6994  disjen  7694  map2xp  7707  ac6sfi  7784  ixpfi2  7838  elfi2  7894  fisn  7907  unxpwdom2  8035  cantnfp1lem3  8120  cantnfp1lem3OLD  8146  isfin4-3  8716  dcomex  8848  iundom2g  8936  fpwwe2lem13  9041  canthp1lem2  9052  0tsk  9154  elreal2  9530  ax1rid  9559  ltxrlt  9676  un0addcl  10854  un0mulcl  10855  elfzonlteqm1  11891  seqf1o  12148  seqid3  12151  seqz  12155  1exp  12195  hashnn0pnf  12415  hashprg  12460  eqs1  12621  cats1un  12701  fsumss  13547  sumsn  13563  fsum2dlem  13585  fsumcom2  13589  ackbijnn  13640  fprodss  13755  fprod2dlem  13784  fprodcom2  13788  phi1  14303  dfphi2  14304  nnnn0modprm0  14331  ramubcl  14536  0ram  14538  ramz  14543  imasvscafn  14934  xpsc0  14957  xpsc1  14958  xpsfrnel2  14962  mreexmrid  15040  gsumress  15903  gsumval2  15907  0nsg  16246  symgextf1lem  16445  symgextf1  16446  pmtrprfval  16512  psgnsn  16545  lsmdisj2  16700  subgdisj1  16709  lt6abl  16897  gsumsnfd  16978  gsumzunsnd  16982  gsumunsnfd  16983  gsum2dlem2  16998  gsum2dOLD  17000  dprdfeq0  17062  dprdfeq0OLD  17069  dprdsn  17083  dprd2da  17091  pgpfac1lem3a  17127  pgpfaclem2  17133  lsssn0  17594  lspsneq0  17658  lspdisjb  17772  lbsextlem4  17807  0ring01eq  17919  mplcoe5  18131  mplcoe2OLD  18133  coe1tm  18314  frgpcyg  18612  obselocv  18759  obs2ss  18760  obslbs  18761  mat0dim0  18969  mat0dimid  18970  mat0dimscm  18971  mat1dimscm  18977  mavmul0g  19055  mdet0pr  19094  mdetunilem9  19122  cramer0  19192  pmatcollpw3fi1lem1  19287  basdif0  19454  ordtbas  19693  ordtrest2  19705  cmpfi  19908  refun0  20016  txdis1cn  20136  ptrescn  20140  txkgen  20153  xkoptsub  20155  ordthmeolem  20302  pt1hmeo  20307  filcon  20384  filufint  20421  flimclslem  20485  ptcmplem3  20554  idnghm  21250  iccpnfcnv  21444  iccpnfhmeo  21445  bndth  21458  ivthicc  21870  ovoliunlem1  21913  i1fima2sn  22087  i1f1  22097  itg1addlem4  22106  itg1addlem5  22107  i1fmulc  22110  limcres  22290  limccnp  22295  limccnp2  22296  degltlem1  22472  ply1rem  22564  fta1blem  22569  ig1pdvds  22577  plyeq0lem  22607  plypf1  22609  plyaddlem1  22610  plymullem1  22611  coemulhi  22651  plycj  22674  taylfval  22754  abelthlem3  22828  rlimcnp  23295  wilthlem2  23343  logexprlim  23500  tgldim0eq  23894  nbcusgra  24463  uvtxnbgra  24493  clwlkisclwwlklem2a4  24784  vdgr1d  24903  vdgr1b  24904  vdgr1a  24906  eupap1  24976  frgraunss  24995  vdgfrgragt2  25027  frgrancvvdeqlemC  25039  frgrawopreglem2  25045  gidsn  25350  rngosn  25406  rngoueqz  25432  xrge0tsmsbi  27776  ordtrest2NEW  27905  xrge0iifcnv  27915  xrge0iifhom  27919  qqhval2  27963  esumsn  28072  esumpr  28073  measvunilem0  28184  measvuni  28185  plymulx0  28504  derangsn  28614  subfacp1lem5  28628  erdszelem4  28638  erdszelem8  28642  sconpi1  28684  cvmlift2lem6  28753  cvmlift2lem12  28759  onint1  29914  tan2h  30047  ptrest  30048  prdsbnd  30289  rrnequiv  30331  grpokerinj  30347  0rngo  30424  isdmn3  30471  hbtlem5  31077  flcidc  31123  radcnvrat  31195  sumsnd  31401  fnchoice  31404  sumsnf  31570  fsumsplitsn  31571  fprodsplitsn  31592  cncfiooicc  31697  fperdvper  31715  dvnmul  31740  dvmptfprodlem  31741  dvnprodlem1  31743  dvnprodlem2  31744  itgcoscmulx  31768  stoweidlem44  31826  wallispi  31852  fourierdlem49  31938  fourierdlem56  31945  fourierdlem80  31969  fourierdlem93  31982  fourierdlem101  31990  eldmressn  32208  2initoinv  32616  2termoinv  32623  c0snmgmhm  32720  zrinitorngc  32808  ldepspr  33074  lmod1zr  33094  unisnALT  33726  bnj142OLD  33781  bnj98  33925  bnj1442  34105  bnj1452  34108  bj-1nel0  34510  bj-sngltag  34541  bj-projval  34554  dibelval2nd  36879  hdmaprnlem9N  37587  hdmap14lem4a  37601
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-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-sn 4030
  Copyright terms: Public domain W3C validator