Theorem velsn 3587

Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
velsn	|- ( x e. { A } <-> x = A )

Proof of Theorem velsn

Step	Hyp	Ref	Expression
1		vex 2724	. 2 |- x e. _V
2	1	elsn 3586	1 |- ( x e. { A } <-> x = A )

Syntax hints:   <-> wb 104   = wceq 1342   e. wcel 2135   {csn 3570

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 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2723  df-sn 3576

This theorem is referenced by:  dfpr2  3589  mosn  3606  ralsnsg  3607  ralsns  3608  rexsns  3609  disjsn  3632  snprc  3635  euabsn2  3639  prmg  3691  snss  3696  difprsnss  3705  eqsnm  3729  snsssn  3735  snsspw  3738  dfnfc2  3801  uni0b  3808  uni0c  3809  sndisj  3972  unidif0  4140  exmid01  4171  rext  4187  exss  4199  frirrg  4322  ordsucim  4471  ordtriexmidlem  4490  ordtri2or2exmidlem  4497  onsucelsucexmidlem  4500  elirr  4512  sucprcreg  4520  fconstmpt  4645  opeliunxp  4653  dmsnopg  5069  dfmpt3  5304  nfunsn  5514  fsn  5651  fnasrn  5657  fnasrng  5659  fconstfvm  5697  eusvobj2  5822  opabex3d  6081  opabex3  6082  dcdifsnid  6463  ecexr  6497  ixp0x  6683  xpsnen  6778  fidifsnen  6827  difinfsn  7056  exmidonfinlem  7140  iccid  9852  fzsn  9991  fzpr  10002  fzdifsuc  10006  fsum2dlemstep  11361  prodsnf  11519  fprod1p  11526  fprodunsn  11531  fprod2dlemstep  11549  ef0lem  11587  1nprm  12025  restsn  12721