Theorem velsn 3392

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

Syntax hints:   ↔ wb 98   = wceq 1243   ∈ wcel 1393  {csn 3375

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-sn 3381

This theorem is referenced by:  dfpr2  3394  mosn  3406  ralsnsg  3407  ralsns  3408  rexsns  3409  rexsnsOLD  3410  disjsn  3432  snprc  3435  euabsn2  3439  prmg  3489  snss  3494  difprsnss  3502  eqsnm  3526  snsssn  3532  snsspw  3535  dfnfc2  3598  uni0b  3605  uni0c  3606  sndisj  3760  unidif0  3920  rext  3951  exss  3963  frirrg  4087  ordsucim  4226  ordtriexmidlem  4245  ordtri2or2exmidlem  4251  onsucelsucexmidlem  4254  elirr  4266  sucprcreg  4273  fconstmpt  4387  opeliunxp  4395  dmsnopg  4792  dfmpt3  5021  nfunsn  5207  fsn  5335  fnasrn  5341  fnasrng  5343  fconstfvm  5379  eusvobj2  5498  opabex3d  5748  opabex3  5749  nndifsnid  6080  ecexr  6111  xpsnen  6295  fidifsnen  6331  fidifsnid  6332  iccid  8794  fzsn  8929  fzpr  8939  fzdifsuc  8943