Theorem elsni 3691

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2202   {csn 3673

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-sn 3679

This theorem is referenced by:  elsn2g  3706  nelsn  3708  disjsn2  3736  rabsnifsb  3741  rabsnif  3742  sssnm  3842  disjxsn  4091  pwntru  4295  opth1  4334  elsuci  4506  ordtri2orexmid  4627  onsucsssucexmid  4631  sosng  4805  elrelimasn  5109  ressn  5284  funcnvsn  5382  funinsn  5386  funopdmsn  5842  fvconst  5850  fmptap  5852  fmptapd  5853  fvunsng  5856  mposnif  6125  1stconst  6395  2ndconst  6396  reldmtpos  6462  tpostpos  6473  1domsn  7044  ac6sfi  7130  elssdc  7137  onunsnss  7152  snon0  7177  snexxph  7192  elfi2  7231  supsnti  7264  djuf1olem  7312  eldju2ndl  7331  eldju2ndr  7332  difinfsnlem  7358  pw1m  7502  pw1on  7504  elreal2  8110  ax1rid  8157  ltxrlt  8304  un0addcl  9494  un0mulcl  9495  fzodisjsn  10481  elfzonlteqm1  10518  xnn0nnen  10762  fxnn0nninf  10764  seqf1og  10846  1exp  10893  hashinfuni  11102  hashennnuni  11104  hashprg  11135  zfz1isolemiso  11166  cats1un  11368  fisumss  12033  sumsnf  12050  fsumsplitsn  12051  fsum2dlemstep  12075  fisumcom2  12079  fprodssdc  12231  fprodunsn  12245  fprod2dlemstep  12263  fprodcom2fi  12267  fprodsplitsn  12274  divalgmod  12568  phi1  12871  dfphi2  12872  nnnn0modprm0  12908  exmidunben  13127  bassetsnn  13219  gsumress  13558  0nsg  13881  gsumfzsnfd  14012  lsssn0  14466  lspsneq0  14522  txdis1cn  15089  plyaddlem1  15558  plymullem1  15559  plycoeid3  15568  plycj  15572  pw0ss  16024  usgr1vr  16189  bj-nntrans  16667  bj-nnelirr  16669  pwtrufal  16719  sssneq  16724  exmidsbthrlem  16750  gfsumsn  16814