Theorem velsn 3650

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

Syntax hints:   ↔ wb 105   = wceq 1373   ∈ wcel 2176  {csn 3633

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-sn 3639

This theorem is referenced by:  dfpr2  3652  mosn  3669  ralsnsg  3670  ralsns  3671  rexsns  3672  disjsn  3695  snprc  3698  euabsn2  3702  prmg  3754  snssOLD  3759  snssb  3766  difprsnss  3771  eqsnm  3796  snsssn  3802  snsspw  3805  dfnfc2  3868  uni0b  3875  uni0c  3876  sndisj  4041  unidif0  4212  exmid01  4243  rext  4260  exss  4272  frirrg  4398  ordsucim  4549  ordtriexmidlem  4568  ordtri2or2exmidlem  4575  onsucelsucexmidlem  4578  elirr  4590  sucprcreg  4598  fconstmpt  4723  opeliunxp  4731  restidsing  5016  dmsnopg  5155  dfmpt3  5400  nfunsn  5613  fsn  5754  fnasrn  5760  fnasrng  5762  fconstfvm  5804  eusvobj2  5932  opabex3d  6208  opabex3  6209  dcdifsnid  6592  ecexr  6627  ixp0x  6815  xpsnen  6918  fidifsnen  6969  difinfsn  7204  exmidonfinlem  7303  iccid  10049  fzsn  10190  fzpr  10201  fzdifsuc  10205  fsum2dlemstep  11778  prodsnf  11936  fprod1p  11943  fprodunsn  11948  fprod2dlemstep  11966  ef0lem  12004  1nprm  12469  mgmidsssn0  13249  mnd1id  13321  0subm  13349  trivsubgsnd  13570  kerf1ghm  13643  mulgrhm2  14405  restsn  14685  lgsquadlem1  15587  lgsquadlem2  15588