Theorem velsn 3609

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

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

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 2739  df-sn 3598

This theorem is referenced by:  dfpr2  3611  mosn  3628  ralsnsg  3629  ralsns  3630  rexsns  3631  disjsn  3654  snprc  3657  euabsn2  3661  prmg  3713  snssOLD  3718  snssb  3725  difprsnss  3730  eqsnm  3755  snsssn  3761  snsspw  3764  dfnfc2  3827  uni0b  3834  uni0c  3835  sndisj  3999  unidif0  4167  exmid01  4198  rext  4215  exss  4227  frirrg  4350  ordsucim  4499  ordtriexmidlem  4518  ordtri2or2exmidlem  4525  onsucelsucexmidlem  4528  elirr  4540  sucprcreg  4548  fconstmpt  4673  opeliunxp  4681  restidsing  4963  dmsnopg  5100  dfmpt3  5338  nfunsn  5549  fsn  5688  fnasrn  5694  fnasrng  5696  fconstfvm  5734  eusvobj2  5860  opabex3d  6121  opabex3  6122  dcdifsnid  6504  ecexr  6539  ixp0x  6725  xpsnen  6820  fidifsnen  6869  difinfsn  7098  exmidonfinlem  7191  iccid  9924  fzsn  10065  fzpr  10076  fzdifsuc  10080  fsum2dlemstep  11441  prodsnf  11599  fprod1p  11606  fprodunsn  11611  fprod2dlemstep  11629  ef0lem  11667  1nprm  12113  mgmidsssn0  12802  mnd1id  12847  0subm  12870  trivsubgsnd  13059  restsn  13650