Theorem elsni 4052

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

Step	Hyp	Ref	Expression
1		elsncg 4050	. 2 |- ( A e. { B } -> ( A e. { B } <-> A = B ) )
2	1	ibi 241	1 |- ( A e. { B } -> A = B )

Syntax hints:   -> wi 4   = wceq 1379   e. wcel 1767   {csn 4027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-sn 4028

This theorem is referenced by:  elsnc2g  4057  elpwunsn  4068  disjsn2  4089  rabsnifsb  4095  sssn  4185  disjxsn  4441  opth1  4720  elsuci  4944  sosn  5069  ressn  5543  funcnvsn  5633  fvconst  6079  fnsnb  6080  fmptap  6084  fmptapd  6085  fvunsn  6093  mpt2snif  6380  1stconst  6871  2ndconst  6872  reldmtpos  6963  tpostpos  6975  disjen  7674  map2xp  7687  ac6sfi  7764  ixpfi2  7818  elfi2  7874  fisn  7887  unxpwdom2  8014  cantnfp1lem3  8099  cantnfp1lem3OLD  8125  isfin4-3  8695  dcomex  8827  iundom2g  8915  fpwwe2lem13  9020  canthp1lem2  9031  0tsk  9133  elreal2  9509  ax1rid  9538  ltxrlt  9655  un0addcl  10829  un0mulcl  10830  elfzonlteqm1  11859  seqf1o  12116  seqid3  12119  seqz  12123  1exp  12163  hashnn0pnf  12383  hashprg  12428  eqs1  12584  cats1un  12664  fsumss  13510  sumsn  13526  fsum2dlem  13548  fsumcom2  13552  ackbijnn  13603  phi1  14162  dfphi2  14163  nnnn0modprm0  14190  ramubcl  14395  0ram  14397  ramz  14402  imasvscafn  14792  xpsc0  14815  xpsc1  14816  xpsfrnel2  14820  mreexmrid  14898  gsumress  15829  gsumval2  15835  0nsg  16051  symgextf1lem  16250  symgextf1  16251  pmtrprfval  16318  psgnsn  16351  lsmdisj2  16506  subgdisj1  16515  lt6abl  16700  gsumsnfd  16781  gsumzunsnd  16785  gsumunsnfd  16786  gsum2dlem2  16801  gsum2dOLD  16803  dprdfeq0  16864  dprdfeq0OLD  16871  dprdsn  16885  dprd2da  16893  pgpfac1lem3a  16929  pgpfaclem2  16935  lsssn0  17394  lspsneq0  17458  lspdisjb  17572  lbsextlem4  17607  0rng01eq  17718  mplcoe5  17930  mplcoe2OLD  17932  coe1tm  18113  frgpcyg  18407  obselocv  18554  obs2ss  18555  obslbs  18556  mat0dim0  18764  mat0dimid  18765  mat0dimscm  18766  mat1dimscm  18772  mavmul0g  18850  mdet0pr  18889  mdetrsca2  18901  mdetrlin2  18904  mdetunilem5  18913  mdetunilem9  18917  cramer0  18987  pmatcollpw3fi1lem1  19082  basdif0  19249  ordtbas  19487  ordtrest2  19499  cmpfi  19702  txdis1cn  19899  ptrescn  19903  txkgen  19916  xkoptsub  19918  ordthmeolem  20065  pt1hmeo  20070  filcon  20147  filufint  20184  flimclslem  20248  ptcmplem3  20317  idnghm  21013  iccpnfcnv  21207  iccpnfhmeo  21208  bndth  21221  ivthicc  21633  ovoliunlem1  21676  i1fima2sn  21850  i1f1  21860  itg1addlem4  21869  itg1addlem5  21870  i1fmulc  21873  limcres  22053  limccnp  22058  limccnp2  22059  degltlem1  22235  ply1rem  22327  fta1blem  22332  ig1pdvds  22340  plyeq0lem  22370  plypf1  22372  plyaddlem1  22373  plymullem1  22374  coemulhi  22413  plycj  22436  taylfval  22516  abelthlem3  22590  rlimcnp  23051  wilthlem2  23099  logexprlim  23256  tgldim0eq  23650  nbcusgra  24167  uvtxnbgra  24197  clwlkisclwwlklem2a4  24488  vdgr1d  24607  vdgr1b  24608  vdgr1a  24610  eupap1  24680  frgraunss  24699  vdgfrgragt2  24732  frgrancvvdeqlemC  24744  frgrawopreglem2  24750  gidsn  25054  rngosn  25110  rngoueqz  25136  gsumsn2  27460  xrge0tsmsbi  27467  ordtrest2NEW  27569  xrge0iifcnv  27579  xrge0iifhom  27583  qqhval2  27627  esumsn  27740  esumpr  27741  measvunilem0  27852  measvuni  27853  plymulx0  28172  derangsn  28282  subfacp1lem5  28296  erdszelem4  28306  erdszelem8  28310  sconpi1  28352  cvmlift2lem6  28421  cvmlift2lem12  28427  fprodss  28685  fprod2dlem  28715  fprodcom2  28719  onint1  29519  tan2h  29652  ptrest  29653  prdsbnd  29920  rrnequiv  29962  grpokerinj  29978  0rngo  30055  isdmn3  30102  hbtlem5  30709  flcidc  30756  sumsnd  31007  fnchoice  31010  cncfiooicc  31261  fperdvper  31276  itgcoscmulx  31315  stoweidlem44  31372  wallispi  31398  fourierdlem49  31484  fourierdlem56  31491  fourierdlem80  31515  fourierdlem101  31536  eldmressn  31703  gsumsndf  32050  ldepspr  32173  lmod1zr  32193  unisnALT  32824  bnj142OLD  32879  bnj98  33022  bnj1442  33202  bnj1452  33205  bj-1nel0  33609  bj-sngltag  33640  bj-projval  33653  dibelval2nd  35967  hdmaprnlem9N  36675  hdmap14lem4a  36689