Theorem velsn 3636

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	⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)

Proof of Theorem velsn

Step	Hyp	Ref	Expression
1		vex 2763	. 2 ⊢ 𝑥 ∈ V
2	1	elsn 3635	1 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)

Syntax hints:   ↔ wb 105   = wceq 1364   ∈ 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:  dfpr2  3638  mosn  3655  ralsnsg  3656  ralsns  3657  rexsns  3658  disjsn  3681  snprc  3684  euabsn2  3688  prmg  3740  snssOLD  3745  snssb  3752  difprsnss  3757  eqsnm  3782  snsssn  3788  snsspw  3791  dfnfc2  3854  uni0b  3861  uni0c  3862  sndisj  4026  unidif0  4197  exmid01  4228  rext  4245  exss  4257  frirrg  4382  ordsucim  4533  ordtriexmidlem  4552  ordtri2or2exmidlem  4559  onsucelsucexmidlem  4562  elirr  4574  sucprcreg  4582  fconstmpt  4707  opeliunxp  4715  restidsing  4999  dmsnopg  5138  dfmpt3  5377  nfunsn  5590  fsn  5731  fnasrn  5737  fnasrng  5739  fconstfvm  5777  eusvobj2  5905  opabex3d  6175  opabex3  6176  dcdifsnid  6559  ecexr  6594  ixp0x  6782  xpsnen  6877  fidifsnen  6928  difinfsn  7161  exmidonfinlem  7255  iccid  9994  fzsn  10135  fzpr  10146  fzdifsuc  10150  fsum2dlemstep  11580  prodsnf  11738  fprod1p  11745  fprodunsn  11750  fprod2dlemstep  11768  ef0lem  11806  1nprm  12255  mgmidsssn0  12970  mnd1id  13031  0subm  13059  trivsubgsnd  13274  kerf1ghm  13347  mulgrhm2  14109  restsn  14359  lgsquadlem1  15234  lgsquadlem2  15235