Theorem velsn 4601

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

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

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 3446  df-sn 4586

This theorem is referenced by:  rabsneq  4604  dfpr2  4606  ralsnsg  4630  rexsns  4631  ralsng  4635  disjsn  4671  snprc  4677  snssb  4742  snssgOLD  4744  raldifsnb  4756  difprsnss  4759  pwpw0  4773  eqsn  4789  eqsndOLD  4791  snsspw  4804  dfnfc2  4889  uni0b  4893  uni0c  4894  iunid  5019  iunsn  5025  sndisj  5094  rext  5403  moabex  5414  exss  5418  otiunsndisj  5475  dffr6  5587  fconstmpt  5693  opeliunxp  5698  opeliun2xp  5699  rnep  5880  restidsing  6013  xpdifid  6129  dmsnopg  6174  sniota  6490  dfmpt3  6634  nfunsn  6882  fnsnfv  6922  dffv2  6938  fsn  7089  fnasrn  7099  fnsnbg  7120  fnsnbOLD  7122  fmptsng  7124  fmptsnd  7125  fvclss  7197  eqfunresadj  7317  eusvobj2  7361  sucexeloniOLD  7766  resf1extb  7890  opabex3d  7923  opabex3rd  7924  opabex3  7925  xpord2pred  8101  xpord3pred  8108  frrlem12  8253  frrlem13  8254  oarec  8503  mapdm0  8792  ixp0x  8876  snmapen  8986  xpsnen  9002  marypha2lem2  9363  elirrv  9525  cantnfp1lem1  9607  cantnfp1lem3  9609  djuunxp  9850  dfac5lem1  10052  dfac5lem2  10053  dfac5lem4  10055  dfac5lem4OLD  10057  fin1a2lem11  10339  axdc4lem  10384  axcclem  10386  ttukeylem7  10444  xrsupexmnf  13241  xrinfmexpnf  13242  iccid  13327  fzsn  13503  fzpr  13516  seqz  13991  hashf1  14398  pr2pwpr  14420  s3iunsndisj  14910  fsum2dlem  15712  incexc2  15780  prodsn  15904  prodsnf  15906  fprod2dlem  15922  ef0lem  16020  lcmfunsnlem2  16586  1nprm  16625  vdwapun  16921  prmodvdslcmf  16994  cshwsiun  17046  mgmidsssn0  18581  mnd1id  18689  0subm  18726  efmnd1bas  18802  smndex1basss  18814  smndex1mgm  18816  trivsubgsnd  19068  kerf1ghm  19161  ghmqusnsglem1  19194  ghmquskerlem1  19197  ghmqusker  19201  symg1bas  19305  pmtrprfvalrn  19402  gex1  19505  sylow2alem1  19531  lsmdisj2  19596  0frgp  19693  0cyg  19807  prmcyg  19808  dprddisj2  19955  ablfacrp  19982  lspdisj  21067  lidlnz  21184  mulgrhm2  21420  pzriprnglem10  21432  ocvin  21616  psrlidm  21904  mplcoe1  21977  mplcoe5  21980  psdmul  22086  maducoeval2  22560  madugsum  22563  en2top  22905  restsn  23090  ist1-3  23269  ordtt1  23299  cmpcld  23322  unisngl  23447  dissnlocfin  23449  ptopn2  23504  snfil  23784  alexsubALTlem2  23968  alexsubALTlem3  23969  alexsubALTlem4  23970  haustsms2  24057  tsmsxplem1  24073  tsmsxplem2  24074  ust0  24140  dscopn  24494  nmoid  24663  limcdif  25810  ellimc2  25811  limcmpt  25817  limcres  25820  ply1remlem  26103  plyeq0lem  26148  plyremlem  26245  aaliou2  26281  radcnv0  26358  abelthlem2  26375  wilthlem2  27012  vmappw  27059  ppinprm  27095  chtnprm  27097  musumsum  27135  dchrhash  27215  lgsquadlem1  27324  lgsquadlem2  27325  ssltsn  27738  eqscut3  27770  ssltleft  27819  ssltright  27820  cofcutr  27872  addsuniflem  27948  negsid  27987  negsunif  28001  ssltmul1  28090  ssltmul2  28091  precsexlem11  28159  onscutlt  28205  n0sfincut  28286  0reno  28401  cplgr1v  29410  rusgrnumwwlkb0  29951  frgrncvvdeq  30288  fusgr2wsp2nb  30313  hsn0elch  31227  cycpmrn  33115  qsxpid  33326  prmidl0  33414  ccfldextdgrr  33660  xrge0iifiso  33918  qqhval2  33965  esumnul  34031  esumrnmpt2  34051  esumfzf  34052  sibfof  34324  sitgaddlemb  34332  plymulx0  34531  signstf0  34552  prodfzo03  34587  circlemeth  34624  sconnpi1  35219  dffr5  35734  elima4  35756  brsingle  35898  dfiota3  35904  funpartfun  35924  dfrdg4  35932  fwddifn0  36145  bj-csbsnlem  36884  bj-axsn  37013  bj-axadj  37022  bj-pw0ALT  37030  bj-restsn  37063  bj-rest10  37069  mptsnunlem  37319  fvineqsneu  37392  matunitlindflem1  37603  poimirlem23  37630  poimirlem26  37633  poimirlem27  37634  grposnOLD  37869  0idl  38012  smprngopr  38039  isdmn3  38061  ressn2  38426  lshpdisj  38973  lsat0cv  39019  snatpsubN  39737  dibelval3  41134  dib1dim  41152  dvh2dim  41432  mapd0  41652  hdmap14lem13  41867  dvrelogpow2b  42049  sticksstones11  42137  unitscyglem4  42179  sn-iotalem  42202  prjspeclsp  42593  pellexlem5  42814  jm2.23  42978  flcidc  43152  tfsconcatrn  43324  snhesn  43768  snssiALTVD  44809  snssiALT  44810  permaxinf2lem  44995  fsneq  45193  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  47849  dfnbgr6  47850  stgredgiun  47950  xpsnopab  48138  mo0sn  48797  tposres0  48858  setcsnterm  49472  2arwcatlem1  49577  2arwcat  49582  setc1onsubc  49584  aacllem  49783