Theorem velsn 3726

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 3725	1 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)

This proof depends on syntax axioms:   ↔ wb 105   = wceq 1402   ∈ wcel 2209  {csn 3709

This proof depends on 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 proof 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 3715

This theorem is used by:  dfpr2  3728  mosn  3745  ralsnsg  3746  ralsns  3747  rexsns  3748  disjsn  3771  snprc  3774  euabsn2  3780  snmb  3834  prmg  3835  snssOLD  3840  snssb  3848  difprsnss  3853  eqsnm  3880  snsssn  3886  snsspw  3889  dfnfc2  3953  uni0b  3960  uni0c  3961  sndisj  4126  sn0disj  4127  unidif0  4306  exmid01  4337  rext  4357  exss  4369  frirrg  4497  ordsucim  4649  ordtriexmidlem  4668  ordtri2or2exmidlem  4675  onsucelsucexmidlem  4678  elirr  4690  sucprcreg  4698  fconstmpt  4824  opeliunxp  4832  restidsing  5122  dmsnopg  5262  dfmpt3  5509  nfunsn  5736  fsn  5883  fnasrn  5890  fnasrng  5892  fconstfvm  5936  eusvobj2  6074  opabex3d  6354  opabex3  6355  dcdifsnid  6781  ecexr  6816  ixp0x  7012  xpsnen  7123  fidifsnen  7176  fissfi  7267  difinfsn  7446  exmidonfinlem  7551  iccid  10344  fzsn  10489  fzpr  10501  fzdifsuc  10505  hashfibc  11305  hashf1  11309  fsum2dlemstep  12226  prodsnf  12384  fprod1p  12391  fprodunsn  12396  fprod2dlemstep  12414  ef0lem  12452  1nprm  12917  mgmidsssn0  13763  mnd1id  13822  0subm  13850  trivsubgsnd  14063  kerf1ghm  14136  mulgrhm2  15054  psrlidmfi  15199  restsn  15406  ppinprm  16260  chtnprm  16262  lgsquadlem1  16401  lgsquadlem2  16402  wexmiddifxylem  17250