Theorem velsn 3722

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

Syntax hints:   ↔ wb 105   = wceq 1402   ∈ wcel 2209  {csn 3705

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-sn 3711

This theorem is referenced by:  dfpr2  3724  mosn  3741  ralsnsg  3742  ralsns  3743  rexsns  3744  disjsn  3767  snprc  3770  euabsn2  3776  snmb  3829  prmg  3830  snssOLD  3835  snssb  3843  difprsnss  3848  eqsnm  3875  snsssn  3881  snsspw  3884  dfnfc2  3948  uni0b  3955  uni0c  3956  sndisj  4121  unidif0  4299  exmid01  4330  rext  4350  exss  4362  frirrg  4490  ordsucim  4642  ordtriexmidlem  4661  ordtri2or2exmidlem  4668  onsucelsucexmidlem  4671  elirr  4683  sucprcreg  4691  fconstmpt  4817  opeliunxp  4825  restidsing  5114  dmsnopg  5254  dfmpt3  5501  nfunsn  5727  fsn  5871  fnasrn  5878  fnasrng  5880  fconstfvm  5924  eusvobj2  6061  opabex3d  6340  opabex3  6341  dcdifsnid  6767  ecexr  6802  ixp0x  6998  xpsnen  7109  fidifsnen  7162  fissfi  7253  difinfsn  7430  exmidonfinlem  7535  iccid  10306  fzsn  10450  fzpr  10462  fzdifsuc  10466  hashfibc  11261  hashf1  11265  fsum2dlemstep  12179  prodsnf  12337  fprod1p  12344  fprodunsn  12349  fprod2dlemstep  12367  ef0lem  12405  1nprm  12870  mgmidsssn0  13681  mnd1id  13740  0subm  13768  trivsubgsnd  13981  kerf1ghm  14054  mulgrhm2  14917  restsn  15204  lgsquadlem1  16110  lgsquadlem2  16111