Theorem elsni 3897

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

Syntax hints:   -> wi 4   = wceq 1369   e. wcel 1756   {csn 3872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-sn 3873

This theorem is referenced by:  elsnc2g  3902  elpwunsn  3912  disjsn2  3932  rabsnifsb  3938  sssn  4026  disjxsn  4281  opth1  4560  elsuci  4780  sosn  4903  ressn  5368  funcnvsn  5458  fvconst  5892  fnsnb  5893  fmptap  5896  fmptapd  5897  fvunsn  5905  mpt2snif  6179  1stconst  6656  2ndconst  6657  reldmtpos  6748  tpostpos  6760  disjen  7460  map2xp  7473  ac6sfi  7548  ixpfi2  7601  elfi2  7656  fisn  7669  unxpwdom2  7795  cantnfp1lem3  7880  cantnfp1lem3OLD  7906  isfin4-3  8476  dcomex  8608  iundom2g  8696  fpwwe2lem13  8801  canthp1lem2  8812  0tsk  8914  elreal2  9291  ax1rid  9320  ltxrlt  9437  un0addcl  10605  un0mulcl  10606  seqf1o  11839  seqid3  11842  seqz  11846  1exp  11885  hashnn0pnf  12105  hashprg  12147  eqs1  12292  cats1un  12362  fsumss  13194  sumsn  13209  fsum2dlem  13229  fsumcom2  13233  ackbijnn  13283  phi1  13840  dfphi2  13841  nnnn0modprm0  13866  ramubcl  14071  0ram  14073  ramz  14078  imasvscafn  14467  xpsc0  14490  xpsc1  14491  xpsfrnel2  14495  mreexmrid  14573  gsumress  15498  gsumval2  15504  0nsg  15717  symgextf1lem  15916  symgextf1  15917  pmtrprfval  15984  lsmdisj2  16170  subgdisj1  16179  lt6abl  16362  gsumsn  16439  gsumsnd  16440  gsumzunsnd  16441  gsumunsnd  16442  gsum2dlem2  16452  gsum2dOLD  16454  dprdfeq0  16502  dprdfeq0OLD  16509  dprdsn  16523  dprd2da  16531  pgpfac1lem3a  16567  pgpfaclem2  16573  lsssn0  17009  lspsneq0  17073  lspdisjb  17187  lbsextlem4  17222  mplcoe5  17528  mplcoe2OLD  17530  coe1tm  17706  frgpcyg  17986  obselocv  18133  obs2ss  18134  obslbs  18135  mavmul0g  18344  mdet0pr  18383  mdetrsca2  18391  mdetrlin2  18393  mdetunilem5  18402  mdetunilem9  18406  cramer0  18476  basdif0  18538  ordtbas  18776  ordtrest2  18788  cmpfi  18991  txdis1cn  19188  ptrescn  19192  txkgen  19205  xkoptsub  19207  ordthmeolem  19354  pt1hmeo  19359  filcon  19436  filufint  19473  flimclslem  19537  ptcmplem3  19606  idnghm  20302  iccpnfcnv  20496  iccpnfhmeo  20497  bndth  20510  ivthicc  20922  ovoliunlem1  20965  i1fima2sn  21138  i1f1  21148  itg1addlem4  21157  itg1addlem5  21158  i1fmulc  21161  limcres  21341  limccnp  21346  limccnp2  21347  degltlem1  21523  ply1rem  21615  fta1blem  21620  ig1pdvds  21628  plyeq0lem  21658  plypf1  21660  plyaddlem1  21661  plymullem1  21662  coemulhi  21701  plycj  21724  taylfval  21804  abelthlem3  21878  rlimcnp  22339  wilthlem2  22387  logexprlim  22544  tgldim0eq  22936  nbcusgra  23339  uvtxnbgra  23369  vdgr1d  23541  vdgr1b  23542  vdgr1a  23544  eupap1  23565  gidsn  23803  rngosn  23859  rngoueqz  23885  gsumsn2  26211  gsumsnf  26212  gsumunsnf  26213  xrge0tsmsbi  26222  ordtrest2NEW  26322  xrge0iifcnv  26332  xrge0iifhom  26336  qqhval2  26380  esumsn  26484  esumpr  26485  measvunilem0  26596  measvuni  26597  plymulx0  26917  derangsn  27027  subfacp1lem5  27041  erdszelem4  27051  erdszelem8  27055  sconpi1  27097  cvmlift2lem6  27166  cvmlift2lem12  27172  fprodss  27430  fprod2dlem  27460  fprodcom2  27464  onint1  28265  tan2h  28395  ptrest  28396  prdsbnd  28663  rrnequiv  28705  grpokerinj  28721  0rngo  28798  isdmn3  28845  hbtlem5  29455  flcidc  29502  sumsnd  29719  fnchoice  29722  stoweidlem44  29810  wallispi  29836  eldmressn  29998  elfzonlteqm1  30196  clwlkisclwwlklem2a4  30417  frgraunss  30558  vdgfrgragt2  30591  frgrancvvdeqlemC  30603  frgrawopreglem2  30609  gsumsndf  30732  psgnsn  30740  0rng01eq  30745  mat0dim0  30823  mat0dimid  30824  mat0dimscm  30825  mat1dimscm  30831  ldepspr  30938  lmod1zr  30966  unisnALT  31591  bnj142OLD  31646  bnj98  31789  bnj1442  31969  bnj1452  31972  bj-1nel0  32345  bj-sngltag  32376  bj-projval  32389  dibelval2nd  34690  hdmaprnlem9N  35398  hdmap14lem4a  35412