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  unidif0  4304  exmid01  4335  rext  4355  exss  4367  frirrg  4495  ordsucim  4647  ordtriexmidlem  4666  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  elirr  4688  sucprcreg  4696  fconstmpt  4822  opeliunxp  4830  restidsing  5119  dmsnopg  5259  dfmpt3  5506  nfunsn  5733  fsn  5880  fnasrn  5887  fnasrng  5889  fconstfvm  5933  eusvobj2  6071  opabex3d  6350  opabex3  6351  dcdifsnid  6777  ecexr  6812  ixp0x  7008  xpsnen  7119  fidifsnen  7172  fissfi  7263  difinfsn  7441  exmidonfinlem  7546  iccid  10338  fzsn  10483  fzpr  10495  fzdifsuc  10499  hashfibc  11299  hashf1  11303  fsum2dlemstep  12220  prodsnf  12378  fprod1p  12385  fprodunsn  12390  fprod2dlemstep  12408  ef0lem  12446  1nprm  12911  mgmidsssn0  13757  mnd1id  13816  0subm  13844  trivsubgsnd  14057  kerf1ghm  14130  mulgrhm2  15029  restsn  15372  ppinprm  16221  chtnprm  16223  lgsquadlem1  16362  lgsquadlem2  16363  wexmiddifxylem  17211