Theorem elsni 3707

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 3704	. 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 2203   {csn 3689

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 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-sn 3695

This theorem is referenced by:  elsn2g  3722  nelsn  3724  disjsn2  3752  rabsnifsb  3757  rabsnif  3758  sssnm  3858  disjxsn  4107  pwntru  4312  opth1  4352  elsuci  4524  ordtri2orexmid  4645  onsucsssucexmid  4649  sosng  4823  elrelimasn  5128  ressn  5303  funcnvsn  5401  funinsn  5405  funopdmsn  5864  fvconst  5872  fmptap  5874  fmptapd  5875  fvunsng  5878  mposnif  6147  1stconst  6417  2ndconst  6418  reldmtpos  6484  tpostpos  6495  1domsn  7068  ac6sfi  7155  elssdc  7162  onunsnss  7177  snon0  7202  snexxph  7220  elfi2  7259  supsnti  7296  djuf1olem  7344  eldju2ndl  7363  eldju2ndr  7364  difinfsnlem  7390  pw1m  7534  pw1on  7536  elreal2  8145  ax1rid  8192  ltxrlt  8339  un0addcl  9529  un0mulcl  9530  fzodisjsn  10518  elfzonlteqm1  10555  xnn0nnen  10799  fxnn0nninf  10801  seqf1og  10883  1exp  10930  hashinfuni  11140  hashennnuni  11142  hashprg  11173  zfz1isolemiso  11211  cats1un  11413  fisumss  12078  sumsnf  12095  fsumsplitsn  12096  fsum2dlemstep  12120  fisumcom2  12124  fprodssdc  12276  fprodunsn  12290  fprod2dlemstep  12308  fprodcom2fi  12312  fprodsplitsn  12319  divalgmod  12613  phi1  12916  dfphi2  12917  nnnn0modprm0  12953  exmidunben  13177  bassetsnn  13269  gsumress  13608  0nsg  13931  gsumfzsnfd  14062  lsssn0  14518  lspsneq0  14574  txdis1cn  15143  plyaddlem1  15612  plymullem1  15613  plycoeid3  15622  plycj  15626  pw0ss  16078  usgr1vr  16243  bj-nntrans  16721  bj-nnelirr  16723  pwtrufal  16771  sssneq  16776  exmidsbthrlem  16802  gfsumsn  16867