Theorem velsn 3655

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 2776	. 2 ⊢ 𝑥 ∈ V
2	1	elsn 3654	1 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)

Syntax hints:   ↔ wb 105   = wceq 1373   ∈ wcel 2177  {csn 3638

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-sn 3644

This theorem is referenced by:  dfpr2  3657  mosn  3674  ralsnsg  3675  ralsns  3676  rexsns  3677  disjsn  3700  snprc  3703  euabsn2  3707  snmb  3759  prmg  3760  snssOLD  3765  snssb  3772  difprsnss  3777  eqsnm  3804  snsssn  3810  snsspw  3813  dfnfc2  3877  uni0b  3884  uni0c  3885  sndisj  4050  unidif0  4222  exmid01  4253  rext  4272  exss  4284  frirrg  4410  ordsucim  4561  ordtriexmidlem  4580  ordtri2or2exmidlem  4587  onsucelsucexmidlem  4590  elirr  4602  sucprcreg  4610  fconstmpt  4735  opeliunxp  4743  restidsing  5029  dmsnopg  5168  dfmpt3  5413  nfunsn  5629  fsn  5770  fnasrn  5776  fnasrng  5778  fconstfvm  5820  eusvobj2  5948  opabex3d  6224  opabex3  6225  dcdifsnid  6608  ecexr  6643  ixp0x  6831  xpsnen  6936  fidifsnen  6988  difinfsn  7223  exmidonfinlem  7327  iccid  10077  fzsn  10218  fzpr  10229  fzdifsuc  10233  fsum2dlemstep  11830  prodsnf  11988  fprod1p  11995  fprodunsn  12000  fprod2dlemstep  12018  ef0lem  12056  1nprm  12521  mgmidsssn0  13301  mnd1id  13373  0subm  13401  trivsubgsnd  13622  kerf1ghm  13695  mulgrhm2  14457  restsn  14737  lgsquadlem1  15639  lgsquadlem2  15640