Theorem elsni 3628

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

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2160   {csn 3610

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-sn 3616

This theorem is referenced by:  elsn2g  3643  nelsn  3645  disjsn2  3673  sssnm  3772  disjxsn  4019  pwntru  4220  opth1  4257  elsuci  4424  ordtri2orexmid  4543  onsucsssucexmid  4547  sosng  4720  elrelimasn  5015  ressn  5190  funcnvsn  5283  funinsn  5287  fvconst  5728  fmptap  5730  fmptapd  5731  fvunsng  5734  mposnif  5994  1stconst  6250  2ndconst  6251  reldmtpos  6282  tpostpos  6293  1domsn  6849  ac6sfi  6930  onunsnss  6949  snon0  6969  snexxph  6983  elfi2  7005  supsnti  7038  djuf1olem  7086  eldju2ndl  7105  eldju2ndr  7106  difinfsnlem  7132  pw1on  7260  elreal2  7864  ax1rid  7911  ltxrlt  8059  un0addcl  9245  un0mulcl  9246  elfzonlteqm1  10247  xnn0nnen  10475  fxnn0nninf  10477  1exp  10590  hashinfuni  10799  hashennnuni  10801  hashprg  10830  zfz1isolemiso  10861  fisumss  11442  sumsnf  11459  fsumsplitsn  11460  fsum2dlemstep  11484  fisumcom2  11488  fprodssdc  11640  fprodunsn  11654  fprod2dlemstep  11672  fprodcom2fi  11676  fprodsplitsn  11683  divalgmod  11974  phi1  12263  dfphi2  12264  nnnn0modprm0  12299  exmidunben  12489  gsumress  12882  0nsg  13179  lsssn0  13712  lspsneq0  13768  txdis1cn  14264  bj-nntrans  15207  bj-nnelirr  15209  pwtrufal  15252  sssneq  15256  exmidsbthrlem  15276