Theorem velsn 3447

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

Syntax hints:   ↔ wb 103   = wceq 1287   ∈ wcel 1436  {csn 3430

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-sn 3436

This theorem is referenced by:  dfpr2  3449  mosn  3461  ralsnsg  3462  ralsns  3463  rexsns  3464  disjsn  3486  snprc  3489  euabsn2  3493  prmg  3543  snss  3548  difprsnss  3557  eqsnm  3581  snsssn  3587  snsspw  3590  dfnfc2  3653  uni0b  3660  uni0c  3661  sndisj  3815  unidif0  3975  exmid01  4004  rext  4014  exss  4026  frirrg  4149  ordsucim  4288  ordtriexmidlem  4307  ordtri2or2exmidlem  4313  onsucelsucexmidlem  4316  elirr  4328  sucprcreg  4336  fconstmpt  4451  opeliunxp  4459  dmsnopg  4864  dfmpt3  5097  nfunsn  5294  fsn  5425  fnasrn  5431  fnasrng  5433  fconstfvm  5469  eusvobj2  5592  opabex3d  5842  opabex3  5843  dcdifsnid  6210  ecexr  6242  xpsnen  6482  fidifsnen  6531  iccid  9267  fzsn  9403  fzpr  9413  fzdifsuc  9417  1nprm  10962