Theorem velsn 3684

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 2803	. 2 |- x e. _V
2	1	elsn 3683	1 |- ( x e. { A } <-> x = A )

Syntax hints:   <-> wb 105   = wceq 1395   e. wcel 2200   {csn 3667

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-sn 3673

This theorem is referenced by:  dfpr2  3686  mosn  3703  ralsnsg  3704  ralsns  3705  rexsns  3706  disjsn  3729  snprc  3732  euabsn2  3738  snmb  3791  prmg  3792  snssOLD  3797  snssb  3804  difprsnss  3809  eqsnm  3836  snsssn  3842  snsspw  3845  dfnfc2  3909  uni0b  3916  uni0c  3917  sndisj  4082  unidif0  4255  exmid01  4286  rext  4305  exss  4317  frirrg  4445  ordsucim  4596  ordtriexmidlem  4615  ordtri2or2exmidlem  4622  onsucelsucexmidlem  4625  elirr  4637  sucprcreg  4645  fconstmpt  4771  opeliunxp  4779  restidsing  5067  dmsnopg  5206  dfmpt3  5452  nfunsn  5672  fsn  5815  fnasrn  5821  fnasrng  5823  fconstfvm  5867  eusvobj2  5999  opabex3d  6278  opabex3  6279  dcdifsnid  6667  ecexr  6702  ixp0x  6890  xpsnen  7000  fidifsnen  7052  difinfsn  7290  exmidonfinlem  7394  iccid  10150  fzsn  10291  fzpr  10302  fzdifsuc  10306  fsum2dlemstep  11985  prodsnf  12143  fprod1p  12150  fprodunsn  12155  fprod2dlemstep  12173  ef0lem  12211  1nprm  12676  mgmidsssn0  13457  mnd1id  13529  0subm  13557  trivsubgsnd  13778  kerf1ghm  13851  mulgrhm2  14614  restsn  14894  lgsquadlem1  15796  lgsquadlem2  15797