Theorem velsn 3606

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

Syntax hints:   ↔ wb 105   = wceq 1353   ∈ wcel 2146  {csn 3589

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-sn 3595

This theorem is referenced by:  dfpr2  3608  mosn  3625  ralsnsg  3626  ralsns  3627  rexsns  3628  disjsn  3651  snprc  3654  euabsn2  3658  prmg  3710  snssOLD  3715  snssb  3722  difprsnss  3727  eqsnm  3751  snsssn  3757  snsspw  3760  dfnfc2  3823  uni0b  3830  uni0c  3831  sndisj  3994  unidif0  4162  exmid01  4193  rext  4209  exss  4221  frirrg  4344  ordsucim  4493  ordtriexmidlem  4512  ordtri2or2exmidlem  4519  onsucelsucexmidlem  4522  elirr  4534  sucprcreg  4542  fconstmpt  4667  opeliunxp  4675  restidsing  4956  dmsnopg  5092  dfmpt3  5330  nfunsn  5541  fsn  5680  fnasrn  5686  fnasrng  5688  fconstfvm  5726  eusvobj2  5851  opabex3d  6112  opabex3  6113  dcdifsnid  6495  ecexr  6530  ixp0x  6716  xpsnen  6811  fidifsnen  6860  difinfsn  7089  exmidonfinlem  7182  iccid  9896  fzsn  10036  fzpr  10047  fzdifsuc  10051  fsum2dlemstep  11410  prodsnf  11568  fprod1p  11575  fprodunsn  11580  fprod2dlemstep  11598  ef0lem  11636  1nprm  12081  mgmidsssn0  12678  mnd1id  12720  0subm  12742  restsn  13260