Theorem velsn 3549

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

Syntax hints:   ↔ wb 104   = wceq 1332   ∈ wcel 1481  {csn 3532

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-sn 3538

This theorem is referenced by:  dfpr2  3551  mosn  3567  ralsnsg  3568  ralsns  3569  rexsns  3570  disjsn  3593  snprc  3596  euabsn2  3600  prmg  3652  snss  3657  difprsnss  3666  eqsnm  3690  snsssn  3696  snsspw  3699  dfnfc2  3762  uni0b  3769  uni0c  3770  sndisj  3933  unidif0  4099  exmid01  4129  rext  4145  exss  4157  frirrg  4280  ordsucim  4424  ordtriexmidlem  4443  ordtri2or2exmidlem  4449  onsucelsucexmidlem  4452  elirr  4464  sucprcreg  4472  fconstmpt  4594  opeliunxp  4602  dmsnopg  5018  dfmpt3  5253  nfunsn  5463  fsn  5600  fnasrn  5606  fnasrng  5608  fconstfvm  5646  eusvobj2  5768  opabex3d  6027  opabex3  6028  dcdifsnid  6408  ecexr  6442  ixp0x  6628  xpsnen  6723  fidifsnen  6772  difinfsn  6993  exmidonfinlem  7066  iccid  9738  fzsn  9877  fzpr  9888  fzdifsuc  9892  fsum2dlemstep  11235  ef0lem  11403  1nprm  11831  restsn  12388