Theorem velsn 3683

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

Syntax hints:   ↔ wb 105   = wceq 1395   ∈ wcel 2200  {csn 3666

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-sn 3672

This theorem is referenced by:  dfpr2  3685  mosn  3702  ralsnsg  3703  ralsns  3704  rexsns  3705  disjsn  3728  snprc  3731  euabsn2  3735  snmb  3788  prmg  3789  snssOLD  3794  snssb  3801  difprsnss  3806  eqsnm  3833  snsssn  3839  snsspw  3842  dfnfc2  3906  uni0b  3913  uni0c  3914  sndisj  4079  unidif0  4251  exmid01  4282  rext  4301  exss  4313  frirrg  4441  ordsucim  4592  ordtriexmidlem  4611  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  elirr  4633  sucprcreg  4641  fconstmpt  4766  opeliunxp  4774  restidsing  5061  dmsnopg  5200  dfmpt3  5446  nfunsn  5666  fsn  5809  fnasrn  5815  fnasrng  5817  fconstfvm  5861  eusvobj2  5993  opabex3d  6272  opabex3  6273  dcdifsnid  6658  ecexr  6693  ixp0x  6881  xpsnen  6988  fidifsnen  7040  difinfsn  7278  exmidonfinlem  7382  iccid  10133  fzsn  10274  fzpr  10285  fzdifsuc  10289  fsum2dlemstep  11961  prodsnf  12119  fprod1p  12126  fprodunsn  12131  fprod2dlemstep  12149  ef0lem  12187  1nprm  12652  mgmidsssn0  13433  mnd1id  13505  0subm  13533  trivsubgsnd  13754  kerf1ghm  13827  mulgrhm2  14590  restsn  14870  lgsquadlem1  15772  lgsquadlem2  15773