Theorem velsn 3711

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

Syntax hints:   ↔ wb 105   = wceq 1398   ∈ wcel 2205  {csn 3694

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-sn 3700

This theorem is referenced by:  dfpr2  3713  mosn  3730  ralsnsg  3731  ralsns  3732  rexsns  3733  disjsn  3756  snprc  3759  euabsn2  3765  snmb  3818  prmg  3819  snssOLD  3824  snssb  3832  difprsnss  3837  eqsnm  3864  snsssn  3870  snsspw  3873  dfnfc2  3937  uni0b  3944  uni0c  3945  sndisj  4110  unidif0  4285  exmid01  4316  rext  4336  exss  4348  frirrg  4476  ordsucim  4627  ordtriexmidlem  4646  ordtri2or2exmidlem  4653  onsucelsucexmidlem  4656  elirr  4668  sucprcreg  4676  fconstmpt  4802  opeliunxp  4810  restidsing  5099  dmsnopg  5239  dfmpt3  5486  nfunsn  5712  fsn  5854  fnasrn  5861  fnasrng  5863  fconstfvm  5907  eusvobj2  6044  opabex3d  6323  opabex3  6324  dcdifsnid  6750  ecexr  6785  ixp0x  6974  xpsnen  7085  fidifsnen  7138  fissfi  7229  difinfsn  7404  exmidonfinlem  7509  iccid  10277  fzsn  10421  fzpr  10433  fzdifsuc  10437  hashfibc  11232  fsum2dlemstep  12145  prodsnf  12303  fprod1p  12310  fprodunsn  12315  fprod2dlemstep  12333  ef0lem  12371  1nprm  12836  mgmidsssn0  13647  mnd1id  13711  0subm  13739  trivsubgsnd  13954  kerf1ghm  14027  mulgrhm2  14884  restsn  15171  lgsquadlem1  16076  lgsquadlem2  16077