Theorem elsni 4009

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

Syntax hints:   -> wi 4   = wceq 1370   e. wcel 1758   {csn 3984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3078  df-sn 3985

This theorem is referenced by:  elsnc2g  4014  elpwunsn  4024  disjsn2  4044  rabsnifsb  4050  sssn  4138  disjxsn  4393  opth1  4672  elsuci  4892  sosn  5015  ressn  5480  funcnvsn  5570  fvconst  6005  fnsnb  6006  fmptap  6009  fmptapd  6010  fvunsn  6018  mpt2snif  6293  1stconst  6770  2ndconst  6771  reldmtpos  6862  tpostpos  6874  disjen  7577  map2xp  7590  ac6sfi  7666  ixpfi2  7719  elfi2  7774  fisn  7787  unxpwdom2  7913  cantnfp1lem3  7998  cantnfp1lem3OLD  8024  isfin4-3  8594  dcomex  8726  iundom2g  8814  fpwwe2lem13  8919  canthp1lem2  8930  0tsk  9032  elreal2  9409  ax1rid  9438  ltxrlt  9555  un0addcl  10723  un0mulcl  10724  seqf1o  11963  seqid3  11966  seqz  11970  1exp  12009  hashnn0pnf  12229  hashprg  12272  eqs1  12417  cats1un  12487  fsumss  13319  sumsn  13334  fsum2dlem  13354  fsumcom2  13358  ackbijnn  13408  phi1  13965  dfphi2  13966  nnnn0modprm0  13991  ramubcl  14196  0ram  14198  ramz  14203  imasvscafn  14593  xpsc0  14616  xpsc1  14617  xpsfrnel2  14621  mreexmrid  14699  gsumress  15625  gsumval2  15631  0nsg  15844  symgextf1lem  16043  symgextf1  16044  pmtrprfval  16111  psgnsn  16144  lsmdisj2  16299  subgdisj1  16308  lt6abl  16491  gsumsn  16570  gsumsnd  16571  gsumzunsnd  16572  gsumunsnd  16573  gsum2dlem2  16583  gsum2dOLD  16585  dprdfeq0  16633  dprdfeq0OLD  16640  dprdsn  16654  dprd2da  16662  pgpfac1lem3a  16698  pgpfaclem2  16704  lsssn0  17151  lspsneq0  17215  lspdisjb  17329  lbsextlem4  17364  mplcoe5  17671  mplcoe2OLD  17673  coe1tm  17849  frgpcyg  18130  obselocv  18277  obs2ss  18278  obslbs  18279  mavmul0g  18490  mdet0pr  18529  mdetrsca2  18541  mdetrlin2  18544  mdetunilem5  18553  mdetunilem9  18557  cramer0  18627  basdif0  18689  ordtbas  18927  ordtrest2  18939  cmpfi  19142  txdis1cn  19339  ptrescn  19343  txkgen  19356  xkoptsub  19358  ordthmeolem  19505  pt1hmeo  19510  filcon  19587  filufint  19624  flimclslem  19688  ptcmplem3  19757  idnghm  20453  iccpnfcnv  20647  iccpnfhmeo  20648  bndth  20661  ivthicc  21073  ovoliunlem1  21116  i1fima2sn  21290  i1f1  21300  itg1addlem4  21309  itg1addlem5  21310  i1fmulc  21313  limcres  21493  limccnp  21498  limccnp2  21499  degltlem1  21675  ply1rem  21767  fta1blem  21772  ig1pdvds  21780  plyeq0lem  21810  plypf1  21812  plyaddlem1  21813  plymullem1  21814  coemulhi  21853  plycj  21876  taylfval  21956  abelthlem3  22030  rlimcnp  22491  wilthlem2  22539  logexprlim  22696  tgldim0eq  23090  nbcusgra  23522  uvtxnbgra  23552  vdgr1d  23724  vdgr1b  23725  vdgr1a  23727  eupap1  23748  gidsn  23986  rngosn  24042  rngoueqz  24068  gsumsn2  26387  gsumsnf  26388  gsumunsnf  26389  xrge0tsmsbi  26398  ordtrest2NEW  26497  xrge0iifcnv  26507  xrge0iifhom  26511  qqhval2  26555  esumsn  26659  esumpr  26660  measvunilem0  26771  measvuni  26772  plymulx0  27091  derangsn  27201  subfacp1lem5  27215  erdszelem4  27225  erdszelem8  27229  sconpi1  27271  cvmlift2lem6  27340  cvmlift2lem12  27346  fprodss  27604  fprod2dlem  27634  fprodcom2  27638  onint1  28438  tan2h  28571  ptrest  28572  prdsbnd  28839  rrnequiv  28881  grpokerinj  28897  0rngo  28974  isdmn3  29021  hbtlem5  29631  flcidc  29678  sumsnd  29895  fnchoice  29898  stoweidlem44  29986  wallispi  30012  eldmressn  30174  elfzonlteqm1  30372  clwlkisclwwlklem2a4  30593  frgraunss  30734  vdgfrgragt2  30767  frgrancvvdeqlemC  30779  frgrawopreglem2  30785  gsumsndf  30910  0rng01eq  30923  mat0dim0  31028  mat0dimid  31029  mat0dimscm  31030  mat1dimscm  31036  ldepspr  31125  lmod1zr  31153  pmatcollpw3fi1lem1  31258  unisnALT  31979  bnj142OLD  32034  bnj98  32177  bnj1442  32357  bnj1452  32360  bj-1nel0  32762  bj-sngltag  32793  bj-projval  32806  dibelval2nd  35120  hdmaprnlem9N  35828  hdmap14lem4a  35842