Theorem velsn 3686

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

Syntax hints:   ↔ wb 105   = wceq 1397   ∈ wcel 2202  {csn 3669

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-sn 3675

This theorem is referenced by:  dfpr2  3688  mosn  3705  ralsnsg  3706  ralsns  3707  rexsns  3708  disjsn  3731  snprc  3734  euabsn2  3740  snmb  3793  prmg  3794  snssOLD  3799  snssb  3806  difprsnss  3811  eqsnm  3838  snsssn  3844  snsspw  3847  dfnfc2  3911  uni0b  3918  uni0c  3919  sndisj  4084  unidif0  4257  exmid01  4288  rext  4307  exss  4319  frirrg  4447  ordsucim  4598  ordtriexmidlem  4617  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  elirr  4639  sucprcreg  4647  fconstmpt  4773  opeliunxp  4781  restidsing  5069  dmsnopg  5208  dfmpt3  5455  nfunsn  5676  fsn  5819  fnasrn  5826  fnasrng  5828  fconstfvm  5872  eusvobj2  6004  opabex3d  6283  opabex3  6284  dcdifsnid  6672  ecexr  6707  ixp0x  6895  xpsnen  7005  fidifsnen  7057  difinfsn  7299  exmidonfinlem  7404  iccid  10160  fzsn  10301  fzpr  10312  fzdifsuc  10316  fsum2dlemstep  12013  prodsnf  12171  fprod1p  12178  fprodunsn  12183  fprod2dlemstep  12201  ef0lem  12239  1nprm  12704  mgmidsssn0  13485  mnd1id  13557  0subm  13585  trivsubgsnd  13806  kerf1ghm  13879  mulgrhm2  14643  restsn  14923  lgsquadlem1  15825  lgsquadlem2  15826