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  5664  fsn  5807  fnasrn  5813  fnasrng  5815  fconstfvm  5857  eusvobj2  5987  opabex3d  6266  opabex3  6267  dcdifsnid  6650  ecexr  6685  ixp0x  6873  xpsnen  6980  fidifsnen  7032  difinfsn  7267  exmidonfinlem  7371  iccid  10121  fzsn  10262  fzpr  10273  fzdifsuc  10277  fsum2dlemstep  11945  prodsnf  12103  fprod1p  12110  fprodunsn  12115  fprod2dlemstep  12133  ef0lem  12171  1nprm  12636  mgmidsssn0  13417  mnd1id  13489  0subm  13517  trivsubgsnd  13738  kerf1ghm  13811  mulgrhm2  14574  restsn  14854  lgsquadlem1  15756  lgsquadlem2  15757