Theorem velsn 3539

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

Syntax hints:   ↔ wb 104   = wceq 1331   ∈ wcel 1480  {csn 3522

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-v 2683  df-sn 3528

This theorem is referenced by:  dfpr2  3541  mosn  3555  ralsnsg  3556  ralsns  3557  rexsns  3558  disjsn  3580  snprc  3583  euabsn2  3587  prmg  3639  snss  3644  difprsnss  3653  eqsnm  3677  snsssn  3683  snsspw  3686  dfnfc2  3749  uni0b  3756  uni0c  3757  sndisj  3920  unidif0  4086  exmid01  4116  rext  4132  exss  4144  frirrg  4267  ordsucim  4411  ordtriexmidlem  4430  ordtri2or2exmidlem  4436  onsucelsucexmidlem  4439  elirr  4451  sucprcreg  4459  fconstmpt  4581  opeliunxp  4589  dmsnopg  5005  dfmpt3  5240  nfunsn  5448  fsn  5585  fnasrn  5591  fnasrng  5593  fconstfvm  5631  eusvobj2  5753  opabex3d  6012  opabex3  6013  dcdifsnid  6393  ecexr  6427  ixp0x  6613  xpsnen  6708  fidifsnen  6757  difinfsn  6978  exmidonfinlem  7042  iccid  9701  fzsn  9839  fzpr  9850  fzdifsuc  9854  fsum2dlemstep  11196  ef0lem  11355  1nprm  11784  restsn  12338