Theorem velsn 4615

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

Syntax hints:   ↔ wb 206   = wceq 1539   ∈ wcel 2107  {csn 4599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3459  df-sn 4600

This theorem is referenced by:  rabsneq  4618  dfpr2  4620  ralsnsg  4644  rexsns  4645  ralsng  4649  disjsn  4685  snprc  4691  snssb  4756  snssgOLD  4758  raldifsnb  4770  difprsnss  4773  pwpw0  4787  eqsn  4803  eqsndOLD  4805  snsspw  4818  dfnfc2  4903  uni0b  4907  uni0c  4908  iunid  5034  iunsn  5040  sndisj  5109  rext  5421  moabex  5432  exss  5436  otiunsndisj  5493  dffr6  5607  fconstmpt  5714  opeliunxp  5719  opeliun2xp  5720  rnep  5904  restidsing  6038  xpdifid  6155  dmsnopg  6200  sniota  6519  dfmpt3  6669  nfunsn  6915  fnsnfv  6955  dffv2  6971  fsn  7122  fnasrn  7132  fnsnbg  7153  fnsnbOLD  7155  fmptsng  7157  fmptsnd  7158  fvclss  7230  eqfunresadj  7349  eusvobj2  7392  sucexeloniOLD  7799  suceloniOLD  7801  resf1extb  7925  opabex3d  7959  opabex3rd  7960  opabex3  7961  xpord2pred  8139  xpord3pred  8146  frrlem12  8291  frrlem13  8292  wfrlem14OLD  8331  wfrlem15OLD  8332  oarec  8569  mapdm0  8851  ixp0x  8935  snmapen  9047  xpsnen  9064  marypha2lem2  9443  elirrv  9603  cantnfp1lem1  9685  cantnfp1lem3  9687  djuunxp  9928  dfac5lem1  10130  dfac5lem2  10131  dfac5lem4  10133  dfac5lem4OLD  10135  fin1a2lem11  10417  axdc4lem  10462  axcclem  10464  ttukeylem7  10522  xrsupexmnf  13314  xrinfmexpnf  13315  iccid  13399  fzsn  13573  fzpr  13586  seqz  14058  hashf1  14465  pr2pwpr  14487  s3iunsndisj  14976  fsum2dlem  15775  incexc2  15843  prodsn  15967  prodsnf  15969  fprod2dlem  15985  ef0lem  16083  lcmfunsnlem2  16646  1nprm  16685  vdwapun  16981  prmodvdslcmf  17054  cshwsiun  17106  mgmidsssn0  18637  mnd1id  18745  0subm  18782  efmnd1bas  18858  smndex1basss  18870  smndex1mgm  18872  trivsubgsnd  19124  kerf1ghm  19217  ghmqusnsglem1  19250  ghmquskerlem1  19253  ghmqusker  19257  symg1bas  19359  pmtrprfvalrn  19456  gex1  19559  sylow2alem1  19585  lsmdisj2  19650  0frgp  19747  0cyg  19861  prmcyg  19862  dprddisj2  20009  ablfacrp  20036  lspdisj  21073  lidlnz  21190  mulgrhm2  21426  pzriprnglem10  21438  ocvin  21621  psrlidm  21909  mplcoe1  21982  mplcoe5  21985  psdmul  22091  maducoeval2  22565  madugsum  22568  en2top  22910  restsn  23095  ist1-3  23274  ordtt1  23304  cmpcld  23327  unisngl  23452  dissnlocfin  23454  ptopn2  23509  snfil  23789  alexsubALTlem2  23973  alexsubALTlem3  23974  alexsubALTlem4  23975  haustsms2  24062  tsmsxplem1  24078  tsmsxplem2  24079  ust0  24145  dscopn  24499  nmoid  24668  limcdif  25816  ellimc2  25817  limcmpt  25823  limcres  25826  ply1remlem  26109  plyeq0lem  26154  plyremlem  26251  aaliou2  26287  radcnv0  26364  abelthlem2  26381  wilthlem2  27017  vmappw  27064  ppinprm  27100  chtnprm  27102  musumsum  27140  dchrhash  27220  lgsquadlem1  27329  lgsquadlem2  27330  ssltsn  27742  ssltleft  27814  ssltright  27815  cofcutr  27863  addsuniflem  27939  negsid  27978  negsunif  27992  ssltmul1  28078  ssltmul2  28079  precsexlem11  28146  nohalf  28312  0reno  28334  cplgr1v  29343  rusgrnumwwlkb0  29887  frgrncvvdeq  30224  fusgr2wsp2nb  30249  hsn0elch  31163  cycpmrn  33091  qsxpid  33314  prmidl0  33402  ccfldextdgrr  33648  xrge0iifiso  33895  qqhval2  33942  esumnul  34008  esumrnmpt2  34028  esumfzf  34029  sibfof  34301  sitgaddlemb  34309  plymulx0  34508  signstf0  34529  prodfzo03  34564  circlemeth  34601  sconnpi1  35190  dffr5  35700  elima4  35722  brsingle  35864  dfiota3  35870  funpartfun  35890  dfrdg4  35898  fwddifn0  36111  bj-csbsnlem  36850  bj-axsn  36979  bj-axadj  36988  bj-pw0ALT  36996  bj-restsn  37029  bj-rest10  37035  mptsnunlem  37285  fvineqsneu  37358  matunitlindflem1  37569  poimirlem23  37596  poimirlem26  37599  poimirlem27  37600  grposnOLD  37835  0idl  37978  smprngopr  38005  isdmn3  38027  ressn2  38389  lshpdisj  38934  lsat0cv  38980  snatpsubN  39698  dibelval3  41095  dib1dim  41113  dvh2dim  41393  mapd0  41613  hdmap14lem13  41828  dvrelogpow2b  42010  sticksstones11  42098  unitscyglem4  42140  sn-iotalem  42201  prjspeclsp  42567  pellexlem5  42788  jm2.23  42952  flcidc  43126  tfsconcatrn  43298  snhesn  43742  snssiALTVD  44785  snssiALT  44786  permaxinf2lem  44971  fsneq  45164  iccintsng  45486  icoiccdif  45487  limcrecl  45594  lptioo2  45596  lptioo1  45597  limcresiooub  45607  limcresioolb  45608  cnrefiisplem  45794  icccncfext  45852  dvmptfprodlem  45909  dvnprodlem3  45913  dirkercncflem2  46069  fourierdlem40  46112  fourierdlem48  46119  fourierdlem51  46122  fourierdlem62  46133  fourierdlem66  46137  fourierdlem74  46145  fourierdlem75  46146  fourierdlem76  46147  fourierdlem78  46149  fourierdlem79  46150  fourierdlem93  46164  fourierdlem101  46172  fourierdlem103  46174  fourierdlem104  46175  fouriersw  46196  elaa2  46199  etransclem44  46243  rrxsnicc  46265  sge00  46341  absnsb  46992  funressnfv  47008  fsetsniunop  47014  dfdfat2  47093  tz6.12-afv  47138  tz6.12-afv2  47205  otiunsndisjX  47244  iccpartgtl  47366  iccpartgt  47367  iccpartleu  47368  iccpartgel  47369  nnsum4primeseven  47740  nnsum4primesevenALTV  47741  bgoldbtbnd  47749  dfclnbgr6  47795  dfnbgr6  47796  stgredgiun  47878  xpsnopab  48026  mo0sn  48688  tposres0  48746  setcsnterm  49236  2arwcatlem1  49333  2arwcat  49338  setc1onsubc  49340  aacllem  49506