Theorem velsn 3686

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

Syntax hints:   ↔ wb 105   = wceq 1397   ∈ wcel 2202  {csn 3669

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-sn 3675

This theorem is referenced by:  dfpr2  3688  mosn  3705  ralsnsg  3706  ralsns  3707  rexsns  3708  disjsn  3731  snprc  3734  euabsn2  3740  snmb  3793  prmg  3794  snssOLD  3799  snssb  3806  difprsnss  3811  eqsnm  3838  snsssn  3844  snsspw  3847  dfnfc2  3911  uni0b  3918  uni0c  3919  sndisj  4084  unidif0  4257  exmid01  4288  rext  4307  exss  4319  frirrg  4447  ordsucim  4598  ordtriexmidlem  4617  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  elirr  4639  sucprcreg  4647  fconstmpt  4773  opeliunxp  4781  restidsing  5069  dmsnopg  5208  dfmpt3  5455  nfunsn  5676  fsn  5819  fnasrn  5825  fnasrng  5827  fconstfvm  5871  eusvobj2  6003  opabex3d  6282  opabex3  6283  dcdifsnid  6671  ecexr  6706  ixp0x  6894  xpsnen  7004  fidifsnen  7056  difinfsn  7298  exmidonfinlem  7403  iccid  10159  fzsn  10300  fzpr  10311  fzdifsuc  10315  fsum2dlemstep  11994  prodsnf  12152  fprod1p  12159  fprodunsn  12164  fprod2dlemstep  12182  ef0lem  12220  1nprm  12685  mgmidsssn0  13466  mnd1id  13538  0subm  13566  trivsubgsnd  13787  kerf1ghm  13860  mulgrhm2  14623  restsn  14903  lgsquadlem1  15805  lgsquadlem2  15806