Theorem velsn 4593

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {csn 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-sn 4578

This theorem is referenced by:  rabsneq  4596  dfpr2  4598  ralsnsg  4622  rexsns  4623  ralsng  4627  disjsn  4663  snprc  4669  snssb  4734  raldifsnb  4747  difprsnss  4750  pwpw0  4764  eqsn  4780  eqsndOLD  4782  snsspw  4795  dfnfc2  4880  uni0b  4884  uni0c  4885  iunid  5009  iunsn  5015  sndisj  5084  rext  5391  moabex  5402  exss  5406  otiunsndisj  5463  dffr6  5575  fconstmpt  5681  opeliunxp  5686  opeliun2xp  5687  rnep  5869  restidsing  6004  xpdifid  6117  dmsnopg  6162  sniota  6473  dfmpt3  6616  nfunsn  6862  fnsnfv  6902  dffv2  6918  fsn  7069  fnasrn  7079  fnsnbg  7100  fnsnbOLD  7102  fmptsng  7104  fmptsnd  7105  fvclss  7177  eqfunresadj  7297  eusvobj2  7341  resf1extb  7867  opabex3d  7900  opabex3rd  7901  opabex3  7902  xpord2pred  8078  xpord3pred  8085  frrlem12  8230  frrlem13  8231  oarec  8480  mapdm0  8769  ixp0x  8853  snmapen  8963  xpsnen  8978  marypha2lem2  9326  elirrvOLD  9490  cantnfp1lem1  9574  cantnfp1lem3  9576  djuunxp  9817  dfac5lem1  10017  dfac5lem2  10018  dfac5lem4  10020  dfac5lem4OLD  10022  fin1a2lem11  10304  axdc4lem  10349  axcclem  10351  ttukeylem7  10409  xrsupexmnf  13207  xrinfmexpnf  13208  iccid  13293  fzsn  13469  fzpr  13482  seqz  13957  hashf1  14364  pr2pwpr  14386  s3iunsndisj  14875  fsum2dlem  15677  incexc2  15745  prodsn  15869  prodsnf  15871  fprod2dlem  15887  ef0lem  15985  lcmfunsnlem2  16551  1nprm  16590  vdwapun  16886  prmodvdslcmf  16959  cshwsiun  17011  mgmidsssn0  18546  mnd1id  18654  0subm  18691  efmnd1bas  18767  smndex1basss  18779  smndex1mgm  18781  trivsubgsnd  19033  kerf1ghm  19126  ghmqusnsglem1  19159  ghmquskerlem1  19162  ghmqusker  19166  symg1bas  19270  pmtrprfvalrn  19367  gex1  19470  sylow2alem1  19496  lsmdisj2  19561  0frgp  19658  0cyg  19772  prmcyg  19773  dprddisj2  19920  ablfacrp  19947  lspdisj  21032  lidlnz  21149  mulgrhm2  21385  pzriprnglem10  21397  ocvin  21581  psrlidm  21869  mplcoe1  21942  mplcoe5  21945  psdmul  22051  maducoeval2  22525  madugsum  22528  en2top  22870  restsn  23055  ist1-3  23234  ordtt1  23264  cmpcld  23287  unisngl  23412  dissnlocfin  23414  ptopn2  23469  snfil  23749  alexsubALTlem2  23933  alexsubALTlem3  23934  alexsubALTlem4  23935  haustsms2  24022  tsmsxplem1  24038  tsmsxplem2  24039  ust0  24105  dscopn  24459  nmoid  24628  limcdif  25775  ellimc2  25776  limcmpt  25782  limcres  25785  ply1remlem  26068  plyeq0lem  26113  plyremlem  26210  aaliou2  26246  radcnv0  26323  abelthlem2  26340  wilthlem2  26977  vmappw  27024  ppinprm  27060  chtnprm  27062  musumsum  27100  dchrhash  27180  lgsquadlem1  27289  lgsquadlem2  27290  ssltsn  27703  eqscut3  27735  ssltleft  27784  ssltright  27785  cofcutr  27837  addsuniflem  27913  negsid  27952  negsunif  27966  ssltmul1  28055  ssltmul2  28056  precsexlem11  28124  onscutlt  28170  n0sfincut  28251  0reno  28366  cplgr1v  29375  rusgrnumwwlkb0  29916  frgrncvvdeq  30253  fusgr2wsp2nb  30278  hsn0elch  31192  cycpmrn  33086  qsxpid  33300  prmidl0  33388  ccfldextdgrr  33645  xrge0iifiso  33908  qqhval2  33955  esumnul  34021  esumrnmpt2  34041  esumfzf  34042  sibfof  34314  sitgaddlemb  34322  plymulx0  34521  signstf0  34542  prodfzo03  34577  circlemeth  34614  sconnpi1  35222  dffr5  35737  elima4  35759  brsingle  35901  dfiota3  35907  funpartfun  35927  dfrdg4  35935  fwddifn0  36148  bj-csbsnlem  36887  bj-axsn  37016  bj-axadj  37025  bj-pw0ALT  37033  bj-restsn  37066  bj-rest10  37072  mptsnunlem  37322  fvineqsneu  37395  matunitlindflem1  37606  poimirlem23  37633  poimirlem26  37636  poimirlem27  37637  grposnOLD  37872  0idl  38015  smprngopr  38042  isdmn3  38064  ressn2  38429  lshpdisj  38976  lsat0cv  39022  snatpsubN  39739  dibelval3  41136  dib1dim  41154  dvh2dim  41434  mapd0  41654  hdmap14lem13  41869  dvrelogpow2b  42051  sticksstones11  42139  unitscyglem4  42181  sn-iotalem  42204  prjspeclsp  42595  pellexlem5  42816  jm2.23  42979  flcidc  43153  tfsconcatrn  43325  snhesn  43769  snssiALTVD  44810  snssiALT  44811  permaxinf2lem  44996  fsneq  45194  iccintsng  45514  icoiccdif  45515  limcrecl  45620  lptioo2  45622  lptioo1  45623  limcresiooub  45633  limcresioolb  45634  cnrefiisplem  45820  icccncfext  45878  dvmptfprodlem  45935  dvnprodlem3  45939  dirkercncflem2  46095  fourierdlem40  46138  fourierdlem48  46145  fourierdlem51  46148  fourierdlem62  46159  fourierdlem66  46163  fourierdlem74  46171  fourierdlem75  46172  fourierdlem76  46173  fourierdlem78  46175  fourierdlem79  46176  fourierdlem93  46190  fourierdlem101  46198  fourierdlem103  46200  fourierdlem104  46201  fouriersw  46222  elaa2  46225  etransclem44  46269  rrxsnicc  46291  sge00  46367  absnsb  47021  funressnfv  47037  fsetsniunop  47043  dfdfat2  47122  tz6.12-afv  47167  tz6.12-afv2  47234  otiunsndisjX  47273  iccpartgtl  47420  iccpartgt  47421  iccpartleu  47422  iccpartgel  47423  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  bgoldbtbnd  47803  dfclnbgr6  47850  dfnbgr6  47851  stgredgiun  47952  xpsnopab  48151  mo0sn  48810  tposres0  48871  setcsnterm  49485  2arwcatlem1  49590  2arwcat  49595  setc1onsubc  49597  aacllem  49796