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  7440  exmidonfinlem  7545  iccid  10327  fzsn  10472  fzpr  10484  fzdifsuc  10488  hashfibc  11283  hashf1  11287  fsum2dlemstep  12201  prodsnf  12359  fprod1p  12366  fprodunsn  12371  fprod2dlemstep  12389  ef0lem  12427  1nprm  12892  mgmidsssn0  13704  mnd1id  13763  0subm  13791  trivsubgsnd  14004  kerf1ghm  14077  mulgrhm2  14945  restsn  15281  lgsquadlem1  16196  lgsquadlem2  16197  wexmiddifxylem  17045