Theorem velsn 3610

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

Syntax hints:   ↔ wb 105   = wceq 1353   ∈ wcel 2148  {csn 3593

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-sn 3599

This theorem is referenced by:  dfpr2  3612  mosn  3629  ralsnsg  3630  ralsns  3631  rexsns  3632  disjsn  3655  snprc  3658  euabsn2  3662  prmg  3714  snssOLD  3719  snssb  3726  difprsnss  3731  eqsnm  3756  snsssn  3762  snsspw  3765  dfnfc2  3828  uni0b  3835  uni0c  3836  sndisj  4000  unidif0  4168  exmid01  4199  rext  4216  exss  4228  frirrg  4351  ordsucim  4500  ordtriexmidlem  4519  ordtri2or2exmidlem  4526  onsucelsucexmidlem  4529  elirr  4541  sucprcreg  4549  fconstmpt  4674  opeliunxp  4682  restidsing  4964  dmsnopg  5101  dfmpt3  5339  nfunsn  5550  fsn  5689  fnasrn  5695  fnasrng  5697  fconstfvm  5735  eusvobj2  5861  opabex3d  6122  opabex3  6123  dcdifsnid  6505  ecexr  6540  ixp0x  6726  xpsnen  6821  fidifsnen  6870  difinfsn  7099  exmidonfinlem  7192  iccid  9925  fzsn  10066  fzpr  10077  fzdifsuc  10081  fsum2dlemstep  11442  prodsnf  11600  fprod1p  11607  fprodunsn  11612  fprod2dlemstep  11630  ef0lem  11668  1nprm  12114  mgmidsssn0  12803  mnd1id  12848  0subm  12871  trivsubgsnd  13061  restsn  13683