Theorem elsni 3637

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 3634	. 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 3619

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 3625

This theorem is referenced by:  elsn2g  3652  nelsn  3654  disjsn2  3682  sssnm  3781  disjxsn  4028  pwntru  4229  opth1  4266  elsuci  4435  ordtri2orexmid  4556  onsucsssucexmid  4560  sosng  4733  elrelimasn  5032  ressn  5207  funcnvsn  5300  funinsn  5304  fvconst  5747  fmptap  5749  fmptapd  5750  fvunsng  5753  mposnif  6013  1stconst  6276  2ndconst  6277  reldmtpos  6308  tpostpos  6319  1domsn  6875  ac6sfi  6956  onunsnss  6975  snon0  6996  snexxph  7011  elfi2  7033  supsnti  7066  djuf1olem  7114  eldju2ndl  7133  eldju2ndr  7134  difinfsnlem  7160  pw1on  7288  elreal2  7892  ax1rid  7939  ltxrlt  8087  un0addcl  9276  un0mulcl  9277  elfzonlteqm1  10280  xnn0nnen  10511  fxnn0nninf  10513  seqf1og  10595  1exp  10642  hashinfuni  10851  hashennnuni  10853  hashprg  10882  zfz1isolemiso  10913  fisumss  11538  sumsnf  11555  fsumsplitsn  11556  fsum2dlemstep  11580  fisumcom2  11584  fprodssdc  11736  fprodunsn  11750  fprod2dlemstep  11768  fprodcom2fi  11772  fprodsplitsn  11779  divalgmod  12071  phi1  12360  dfphi2  12361  nnnn0modprm0  12396  exmidunben  12586  gsumress  12981  0nsg  13287  gsumfzsnfd  13418  lsssn0  13869  lspsneq0  13925  txdis1cn  14457  plyaddlem1  14926  plymullem1  14927  plycj  14939  bj-nntrans  15513  bj-nnelirr  15515  pwtrufal  15558  sssneq  15562  exmidsbthrlem  15582