Theorem velsn 3726

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

This proof depends on syntax axioms:   <-> wb 105   = wceq 1402   e. wcel 2209   {csn 3709

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-sn 3715

This theorem is used by:  dfpr2  3728  mosn  3745  ralsnsg  3746  ralsns  3747  rexsns  3748  disjsn  3771  snprc  3774  euabsn2  3780  snmb  3834  prmg  3835  snssOLD  3840  snssb  3848  difprsnss  3853  eqsnm  3880  snsssn  3886  snsspw  3889  dfnfc2  3953  uni0b  3960  uni0c  3961  sndisj  4126  sn0disj  4127  unidif0  4306  exmid01  4337  rext  4357  exss  4369  frirrg  4497  ordsucim  4649  ordtriexmidlem  4668  ordtri2or2exmidlem  4675  onsucelsucexmidlem  4678  elirr  4690  sucprcreg  4698  fconstmpt  4824  opeliunxp  4832  restidsing  5122  dmsnopg  5262  dfmpt3  5509  nfunsn  5736  fsn  5883  fnasrn  5890  fnasrng  5892  fconstfvm  5936  eusvobj2  6074  opabex3d  6354  opabex3  6355  dcdifsnid  6782  ecexr  6817  ixp0x  7014  xpsnen  7125  fidifsnen  7178  fissfi  7269  difinfsn  7446  exmidonfinlem  7551  iccid  10343  fzsn  10488  fzpr  10500  fzdifsuc  10504  hashfibc  11304  hashf1  11308  fsum2dlemstep  12225  prodsnf  12383  fprod1p  12390  fprodunsn  12395  fprod2dlemstep  12413  ef0lem  12451  1nprm  12916  mgmidsssn0  13762  mnd1id  13821  0subm  13849  trivsubgsnd  14062  kerf1ghm  14135  mulgrhm2  15053  psrlidmfi  15208  mvrclfi  15226  restsn  15423  ppinprm  16277  chtnprm  16279  lgsquadlem1  16418  lgsquadlem2  16419  wexmiddifxylem  17267