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

Theorem elsni 4035
Description: There is only one element in a singleton. (Contributed by NM, 5-Jun-1994.)
Assertion
Ref Expression
elsni  |-  ( A  e.  { B }  ->  A  =  B )

Proof of Theorem elsni
StepHypRef Expression
1 elsncg 4033 . 2  |-  ( A  e.  { B }  ->  ( A  e.  { B }  <->  A  =  B
) )
21ibi 241 1  |-  ( A  e.  { B }  ->  A  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1381    e. wcel 1802   {csn 4010
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-sn 4011
This theorem is referenced by:  elsnc2g  4040  elpwunsn  4051  disjsn2  4072  rabsnifsb  4079  sssn  4169  disjxsn  4427  opth1  4706  elsuci  4930  sosn  5055  ressn  5529  funcnvsn  5619  fvconst  6070  fnsnb  6071  fmptap  6075  fvunsn  6084  mpt2snif  6377  1stconst  6869  2ndconst  6870  reldmtpos  6961  tpostpos  6973  disjen  7672  map2xp  7685  ac6sfi  7762  ixpfi2  7816  elfi2  7872  fisn  7885  unxpwdom2  8012  cantnfp1lem3  8097  cantnfp1lem3OLD  8123  isfin4-3  8693  dcomex  8825  iundom2g  8913  fpwwe2lem13  9018  canthp1lem2  9029  0tsk  9131  elreal2  9507  ax1rid  9536  ltxrlt  9653  un0addcl  10830  un0mulcl  10831  elfzonlteqm1  11865  seqf1o  12122  seqid3  12125  seqz  12129  1exp  12169  hashnn0pnf  12389  hashprg  12434  eqs1  12595  cats1un  12675  fsumss  13521  sumsn  13537  fsum2dlem  13559  fsumcom2  13563  ackbijnn  13614  phi1  14175  dfphi2  14176  nnnn0modprm0  14203  ramubcl  14408  0ram  14410  ramz  14415  imasvscafn  14806  xpsc0  14829  xpsc1  14830  xpsfrnel2  14834  mreexmrid  14912  gsumress  15772  gsumval2  15776  0nsg  16115  symgextf1lem  16314  symgextf1  16315  pmtrprfval  16381  psgnsn  16414  lsmdisj2  16569  subgdisj1  16578  lt6abl  16766  gsumsnfd  16847  gsumzunsnd  16851  gsumunsnfd  16852  gsum2dlem2  16867  gsum2dOLD  16869  dprdfeq0  16930  dprdfeq0OLD  16937  dprdsn  16951  dprd2da  16959  pgpfac1lem3a  16995  pgpfaclem2  17001  lsssn0  17462  lspsneq0  17526  lspdisjb  17640  lbsextlem4  17675  0ring01eq  17787  mplcoe5  17999  mplcoe2OLD  18001  coe1tm  18182  frgpcyg  18479  obselocv  18626  obs2ss  18627  obslbs  18628  mat0dim0  18836  mat0dimid  18837  mat0dimscm  18838  mat1dimscm  18844  mavmul0g  18922  mdet0pr  18961  mdetunilem9  18989  cramer0  19059  pmatcollpw3fi1lem1  19154  basdif0  19321  ordtbas  19559  ordtrest2  19571  cmpfi  19774  refun0  19882  txdis1cn  20002  ptrescn  20006  txkgen  20019  xkoptsub  20021  ordthmeolem  20168  pt1hmeo  20173  filcon  20250  filufint  20287  flimclslem  20351  ptcmplem3  20420  idnghm  21116  iccpnfcnv  21310  iccpnfhmeo  21311  bndth  21324  ivthicc  21736  ovoliunlem1  21779  i1fima2sn  21953  i1f1  21963  itg1addlem4  21972  itg1addlem5  21973  i1fmulc  21976  limcres  22156  limccnp  22161  limccnp2  22162  degltlem1  22338  ply1rem  22430  fta1blem  22435  ig1pdvds  22443  plyeq0lem  22473  plypf1  22475  plyaddlem1  22476  plymullem1  22477  coemulhi  22516  plycj  22539  taylfval  22619  abelthlem3  22693  rlimcnp  23160  wilthlem2  23208  logexprlim  23365  tgldim0eq  23759  nbcusgra  24328  uvtxnbgra  24358  clwlkisclwwlklem2a4  24649  vdgr1d  24768  vdgr1b  24769  vdgr1a  24771  eupap1  24841  frgraunss  24860  vdgfrgragt2  24892  frgrancvvdeqlemC  24904  frgrawopreglem2  24910  gidsn  25215  rngosn  25271  rngoueqz  25297  xrge0tsmsbi  27642  ordtrest2NEW  27771  xrge0iifcnv  27781  xrge0iifhom  27785  qqhval2  27829  esumsn  27938  esumpr  27939  measvunilem0  28050  measvuni  28051  plymulx0  28370  derangsn  28480  subfacp1lem5  28494  erdszelem4  28504  erdszelem8  28508  sconpi1  28550  cvmlift2lem6  28619  cvmlift2lem12  28625  fprodss  29048  fprod2dlem  29078  fprodcom2  29082  onint1  29882  tan2h  30015  ptrest  30016  prdsbnd  30257  rrnequiv  30299  grpokerinj  30315  0rngo  30392  isdmn3  30439  hbtlem5  31045  flcidc  31092  radcnvrat  31164  sumsnd  31348  fnchoice  31351  cncfiooicc  31600  fperdvper  31615  itgcoscmulx  31654  stoweidlem44  31711  wallispi  31737  fourierdlem49  31823  fourierdlem56  31830  fourierdlem80  31854  fourierdlem93  31867  fourierdlem101  31875  eldmressn  32042  ldepspr  32784  lmod1zr  32804  unisnALT  33434  bnj142OLD  33489  bnj98  33632  bnj1442  33812  bnj1452  33815  bj-1nel0  34222  bj-sngltag  34253  bj-projval  34266  dibelval2nd  36581  hdmaprnlem9N  37289  hdmap14lem4a  37303
  Copyright terms: Public domain W3C validator