Theorem velsn 3419

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

Syntax hints:   ↔ wb 102   = wceq 1259   ∈ wcel 1409  {csn 3402

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038

This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-v 2576  df-sn 3408

This theorem is referenced by:  dfpr2  3421  mosn  3433  ralsnsg  3434  ralsns  3435  rexsns  3436  rexsnsOLD  3437  disjsn  3459  snprc  3462  euabsn2  3466  prmg  3516  snss  3521  difprsnss  3529  eqsnm  3553  snsssn  3559  snsspw  3562  dfnfc2  3625  uni0b  3632  uni0c  3633  sndisj  3787  unidif0  3947  rext  3978  exss  3990  frirrg  4114  ordsucim  4253  ordtriexmidlem  4272  ordtri2or2exmidlem  4278  onsucelsucexmidlem  4281  elirr  4293  sucprcreg  4300  fconstmpt  4414  opeliunxp  4422  dmsnopg  4819  dfmpt3  5048  nfunsn  5234  fsn  5362  fnasrn  5368  fnasrng  5370  fconstfvm  5406  eusvobj2  5525  opabex3d  5775  opabex3  5776  nndifsnid  6110  ecexr  6141  xpsnen  6325  fidifsnen  6361  fidifsnid  6362  iccid  8894  fzsn  9030  fzpr  9040  fzdifsuc  9044