Theorem elsni 4041

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 4039	. 2 |- ( A e. { B } -> ( A e. { B } <-> A = B ) )
2	1	ibi 241	1 |- ( A e. { B } -> A = B )

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 1823   {csn 4016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-sn 4017

This theorem is referenced by:  elsnc2g  4046  elpwunsn  4057  disjsn2  4077  rabsnifsb  4084  sssn  4174  disjxsn  4433  opth1  4710  elsuci  4933  sosn  5058  ressn  5526  funcnvsn  5615  fvconst  6065  fnsnb  6066  fmptap  6070  fvunsn  6079  mpt2snif  6369  1stconst  6861  2ndconst  6862  reldmtpos  6955  tpostpos  6967  disjen  7667  map2xp  7680  ac6sfi  7756  ixpfi2  7810  elfi2  7866  fisn  7879  unxpwdom2  8006  cantnfp1lem3  8090  cantnfp1lem3OLD  8116  isfin4-3  8686  dcomex  8818  iundom2g  8906  fpwwe2lem13  9009  canthp1lem2  9020  0tsk  9122  elreal2  9498  ax1rid  9527  ltxrlt  9644  un0addcl  10825  un0mulcl  10826  elfzonlteqm1  11872  seqf1o  12130  seqid3  12133  seqz  12137  1exp  12177  hashnn0pnf  12397  hashprg  12444  cats1un  12692  fsumss  13629  sumsn  13645  fsum2dlem  13667  fsumcom2  13671  ackbijnn  13722  fprodss  13837  fprod2dlem  13866  fprodcom2  13870  phi1  14387  dfphi2  14388  nnnn0modprm0  14415  ramubcl  14620  0ram  14622  ramz  14627  imasvscafn  15026  xpsc0  15049  xpsc1  15050  xpsfrnel2  15054  mreexmrid  15132  2initoinv  15488  2termoinv  15495  gsumress  16102  gsumval2  16106  0nsg  16445  symgextf1lem  16644  symgextf1  16645  pmtrprfval  16711  psgnsn  16744  lsmdisj2  16899  subgdisj1  16908  lt6abl  17096  gsumsnfd  17174  gsumzunsnd  17178  gsumunsnfd  17179  gsum2dlem2  17194  gsum2dOLD  17196  dprdfeq0  17257  dprdfeq0OLD  17264  dprdsn  17278  dprd2da  17286  pgpfac1lem3a  17322  pgpfaclem2  17328  lsssn0  17789  lspsneq0  17853  lspdisjb  17967  lbsextlem4  18002  0ring01eq  18114  mplcoe5  18326  mplcoe2OLD  18328  coe1tm  18509  frgpcyg  18785  obselocv  18932  obs2ss  18933  obslbs  18934  mat0dim0  19136  mat0dimid  19137  mat0dimscm  19138  mat1dimscm  19144  mavmul0g  19222  mdet0pr  19261  mdetunilem9  19289  cramer0  19359  pmatcollpw3fi1lem1  19454  basdif0  19621  ordtbas  19860  ordtrest2  19872  cmpfi  20075  refun0  20182  txdis1cn  20302  ptrescn  20306  txkgen  20319  xkoptsub  20321  ordthmeolem  20468  pt1hmeo  20473  filcon  20550  filufint  20587  flimclslem  20651  ptcmplem3  20720  idnghm  21416  iccpnfcnv  21610  iccpnfhmeo  21611  bndth  21624  ivthicc  22036  ovoliunlem1  22079  i1fima2sn  22253  i1f1  22263  itg1addlem4  22272  itg1addlem5  22273  i1fmulc  22276  limcres  22456  limccnp  22461  limccnp2  22462  degltlem1  22638  ply1rem  22730  fta1blem  22735  ig1pdvds  22743  plyeq0lem  22773  plypf1  22775  plyaddlem1  22776  plymullem1  22777  coemulhi  22817  plycj  22840  taylfval  22920  abelthlem3  22994  rlimcnp  23493  wilthlem2  23541  logexprlim  23698  tgldim0eq  24095  nbcusgra  24665  uvtxnbgra  24695  clwlkisclwwlklem2a4  24986  vdgr1d  25105  vdgr1b  25106  vdgr1a  25108  eupap1  25178  frgraunss  25197  vdgfrgragt2  25229  frgrancvvdeqlemC  25241  frgrawopreglem2  25247  gidsn  25548  rngosn  25604  rngoueqz  25630  xrge0tsmsbi  28011  ordtrest2NEW  28140  xrge0iifcnv  28150  xrge0iifhom  28154  qqhval2  28197  esumsnf  28293  esumpr  28295  esumiun  28323  measvunilem0  28421  measvuni  28422  carsggect  28526  omsmeas  28531  plymulx0  28768  derangsn  28878  subfacp1lem5  28892  erdszelem4  28902  erdszelem8  28906  sconpi1  28948  cvmlift2lem6  29017  cvmlift2lem12  29023  onint1  30142  tan2h  30287  ptrest  30288  prdsbnd  30529  rrnequiv  30571  grpokerinj  30587  0rngo  30664  isdmn3  30711  hbtlem5  31318  flcidc  31364  radcnvrat  31436  sumsnd  31641  fnchoice  31644  sumsnf  31809  fsumsplitsn  31810  fprodsplitsn  31831  cncfiooicc  31936  fperdvper  31954  dvnmul  31979  dvmptfprodlem  31980  dvnprodlem1  31982  dvnprodlem2  31983  itgcoscmulx  32007  stoweidlem44  32065  wallispi  32091  fourierdlem49  32177  fourierdlem56  32184  fourierdlem80  32208  fourierdlem93  32221  fourierdlem101  32229  eldmressn  32447  c0snmgmhm  32974  zrinitorngc  33062  ldepspr  33328  lmod1zr  33348  unisnALT  34127  bnj142OLD  34182  bnj98  34326  bnj1442  34506  bnj1452  34509  bj-1nel0  34911  bj-sngltag  34942  bj-projval  34955  dibelval2nd  37276  hdmaprnlem9N  37984  hdmap14lem4a  37998