Theorem elsni 3578

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

Syntax hints:   -> wi 4   = wceq 1335   e. wcel 2128   {csn 3560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-v 2714  df-sn 3566

This theorem is referenced by:  elsn2g  3593  nelsn  3595  disjsn2  3623  sssnm  3718  disjxsn  3964  pwntru  4161  opth1  4197  elsuci  4364  ordtri2orexmid  4483  onsucsssucexmid  4487  sosng  4660  ressn  5127  funcnvsn  5216  funinsn  5220  fvconst  5656  fmptap  5658  fmptapd  5659  fvunsng  5662  mposnif  5916  1stconst  6169  2ndconst  6170  reldmtpos  6201  tpostpos  6212  1domsn  6765  ac6sfi  6844  onunsnss  6862  snon0  6881  snexxph  6895  elfi2  6917  supsnti  6950  djuf1olem  6998  eldju2ndl  7017  eldju2ndr  7018  difinfsnlem  7044  pw1on  7162  elreal2  7751  ax1rid  7798  ltxrlt  7944  un0addcl  9124  un0mulcl  9125  elfzonlteqm1  10113  fxnn0nninf  10341  1exp  10452  hashinfuni  10655  hashennnuni  10657  hashprg  10686  zfz1isolemiso  10714  fisumss  11293  sumsnf  11310  fsumsplitsn  11311  fsum2dlemstep  11335  fisumcom2  11339  fprodssdc  11491  fprodunsn  11505  fprod2dlemstep  11523  fprodcom2fi  11527  fprodsplitsn  11534  divalgmod  11822  phi1  12098  dfphi2  12099  nnnn0modprm0  12134  exmidunben  12197  txdis1cn  12720  bj-nntrans  13568  bj-nnelirr  13570  pwtrufal  13611  sssneq  13616  exmidsbthrlem  13635