Theorem velsn 3712

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

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

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 3701

This theorem is referenced by:  dfpr2  3714  mosn  3731  ralsnsg  3732  ralsns  3733  rexsns  3734  disjsn  3757  snprc  3760  euabsn2  3766  snmb  3819  prmg  3820  snssOLD  3825  snssb  3833  difprsnss  3838  eqsnm  3865  snsssn  3871  snsspw  3874  dfnfc2  3938  uni0b  3945  uni0c  3946  sndisj  4111  unidif0  4286  exmid01  4317  rext  4337  exss  4349  frirrg  4477  ordsucim  4629  ordtriexmidlem  4648  ordtri2or2exmidlem  4655  onsucelsucexmidlem  4658  elirr  4670  sucprcreg  4678  fconstmpt  4804  opeliunxp  4812  restidsing  5101  dmsnopg  5241  dfmpt3  5488  nfunsn  5714  fsn  5856  fnasrn  5863  fnasrng  5865  fconstfvm  5909  eusvobj2  6046  opabex3d  6325  opabex3  6326  dcdifsnid  6752  ecexr  6787  ixp0x  6976  xpsnen  7087  fidifsnen  7140  fissfi  7231  difinfsn  7406  exmidonfinlem  7511  iccid  10282  fzsn  10426  fzpr  10438  fzdifsuc  10442  hashfibc  11237  fsum2dlemstep  12151  prodsnf  12309  fprod1p  12316  fprodunsn  12321  fprod2dlemstep  12339  ef0lem  12377  1nprm  12842  mgmidsssn0  13653  mnd1id  13717  0subm  13745  trivsubgsnd  13960  kerf1ghm  14033  mulgrhm2  14890  restsn  15177  lgsquadlem1  16082  lgsquadlem2  16083