Theorem velsn 3600

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

Syntax hints:   ↔ wb 104   = wceq 1348   ∈ wcel 2141  {csn 3583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-sn 3589

This theorem is referenced by:  dfpr2  3602  mosn  3619  ralsnsg  3620  ralsns  3621  rexsns  3622  disjsn  3645  snprc  3648  euabsn2  3652  prmg  3704  snss  3709  difprsnss  3718  eqsnm  3742  snsssn  3748  snsspw  3751  dfnfc2  3814  uni0b  3821  uni0c  3822  sndisj  3985  unidif0  4153  exmid01  4184  rext  4200  exss  4212  frirrg  4335  ordsucim  4484  ordtriexmidlem  4503  ordtri2or2exmidlem  4510  onsucelsucexmidlem  4513  elirr  4525  sucprcreg  4533  fconstmpt  4658  opeliunxp  4666  dmsnopg  5082  dfmpt3  5320  nfunsn  5530  fsn  5668  fnasrn  5674  fnasrng  5676  fconstfvm  5714  eusvobj2  5839  opabex3d  6100  opabex3  6101  dcdifsnid  6483  ecexr  6518  ixp0x  6704  xpsnen  6799  fidifsnen  6848  difinfsn  7077  exmidonfinlem  7170  iccid  9882  fzsn  10022  fzpr  10033  fzdifsuc  10037  fsum2dlemstep  11397  prodsnf  11555  fprod1p  11562  fprodunsn  11567  fprod2dlemstep  11585  ef0lem  11623  1nprm  12068  mgmidsssn0  12638  mnd1id  12680  0subm  12702  restsn  12974