Theorem velsn 3415

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

Syntax hints:   <-> wb 103   = wceq 1284   e. wcel 1433   {csn 3398

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603  df-sn 3404

This theorem is referenced by:  dfpr2  3417  mosn  3429  ralsnsg  3430  ralsns  3431  rexsns  3432  disjsn  3454  snprc  3457  euabsn2  3461  prmg  3511  snss  3516  difprsnss  3524  eqsnm  3547  snsssn  3553  snsspw  3556  dfnfc2  3619  uni0b  3626  uni0c  3627  sndisj  3781  unidif0  3941  rext  3970  exss  3982  frirrg  4105  ordsucim  4244  ordtriexmidlem  4263  ordtri2or2exmidlem  4269  onsucelsucexmidlem  4272  elirr  4284  sucprcreg  4292  fconstmpt  4405  opeliunxp  4413  dmsnopg  4812  dfmpt3  5041  nfunsn  5228  fsn  5356  fnasrn  5362  fnasrng  5364  fconstfvm  5400  eusvobj2  5518  opabex3d  5768  opabex3  5769  nndifsnid  6103  ecexr  6134  xpsnen  6318  fidifsnen  6355  fidifsnid  6356  iccid  8948  fzsn  9084  fzpr  9094  fzdifsuc  9098  1nprm  10496