Theorem elsni 3636

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 3633	. 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 2164   {csn 3618

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 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-sn 3624

This theorem is referenced by:  elsn2g  3651  nelsn  3653  disjsn2  3681  sssnm  3780  disjxsn  4027  pwntru  4228  opth1  4265  elsuci  4434  ordtri2orexmid  4555  onsucsssucexmid  4559  sosng  4732  elrelimasn  5031  ressn  5206  funcnvsn  5299  funinsn  5303  fvconst  5746  fmptap  5748  fmptapd  5749  fvunsng  5752  mposnif  6012  1stconst  6274  2ndconst  6275  reldmtpos  6306  tpostpos  6317  1domsn  6873  ac6sfi  6954  onunsnss  6973  snon0  6994  snexxph  7009  elfi2  7031  supsnti  7064  djuf1olem  7112  eldju2ndl  7131  eldju2ndr  7132  difinfsnlem  7158  pw1on  7286  elreal2  7890  ax1rid  7937  ltxrlt  8085  un0addcl  9273  un0mulcl  9274  elfzonlteqm1  10277  xnn0nnen  10508  fxnn0nninf  10510  seqf1og  10592  1exp  10639  hashinfuni  10848  hashennnuni  10850  hashprg  10879  zfz1isolemiso  10910  fisumss  11535  sumsnf  11552  fsumsplitsn  11553  fsum2dlemstep  11577  fisumcom2  11581  fprodssdc  11733  fprodunsn  11747  fprod2dlemstep  11765  fprodcom2fi  11769  fprodsplitsn  11776  divalgmod  12068  phi1  12357  dfphi2  12358  nnnn0modprm0  12393  exmidunben  12583  gsumress  12978  0nsg  13284  gsumfzsnfd  13415  lsssn0  13866  lspsneq0  13922  txdis1cn  14446  plyaddlem1  14893  plymullem1  14894  bj-nntrans  15443  bj-nnelirr  15445  pwtrufal  15488  sssneq  15492  exmidsbthrlem  15512