Theorem velsn 4608

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-sn 4593

This theorem is referenced by:  rabsneq  4611  dfpr2  4613  ralsnsg  4637  rexsns  4638  ralsng  4642  disjsn  4678  snprc  4684  snssb  4749  snssgOLD  4751  raldifsnb  4763  difprsnss  4766  pwpw0  4780  eqsn  4796  eqsndOLD  4798  snsspw  4811  dfnfc2  4896  uni0b  4900  uni0c  4901  iunid  5027  iunsn  5033  sndisj  5102  rext  5411  moabex  5422  exss  5426  otiunsndisj  5483  dffr6  5597  fconstmpt  5703  opeliunxp  5708  opeliun2xp  5709  rnep  5893  restidsing  6027  xpdifid  6144  dmsnopg  6189  sniota  6505  dfmpt3  6655  nfunsn  6903  fnsnfv  6943  dffv2  6959  fsn  7110  fnasrn  7120  fnsnbg  7141  fnsnbOLD  7143  fmptsng  7145  fmptsnd  7146  fvclss  7218  eqfunresadj  7338  eusvobj2  7382  sucexeloniOLD  7789  resf1extb  7913  opabex3d  7947  opabex3rd  7948  opabex3  7949  xpord2pred  8127  xpord3pred  8134  frrlem12  8279  frrlem13  8280  oarec  8529  mapdm0  8818  ixp0x  8902  snmapen  9012  xpsnen  9029  marypha2lem2  9394  elirrv  9556  cantnfp1lem1  9638  cantnfp1lem3  9640  djuunxp  9881  dfac5lem1  10083  dfac5lem2  10084  dfac5lem4  10086  dfac5lem4OLD  10088  fin1a2lem11  10370  axdc4lem  10415  axcclem  10417  ttukeylem7  10475  xrsupexmnf  13272  xrinfmexpnf  13273  iccid  13358  fzsn  13534  fzpr  13547  seqz  14022  hashf1  14429  pr2pwpr  14451  s3iunsndisj  14941  fsum2dlem  15743  incexc2  15811  prodsn  15935  prodsnf  15937  fprod2dlem  15953  ef0lem  16051  lcmfunsnlem2  16617  1nprm  16656  vdwapun  16952  prmodvdslcmf  17025  cshwsiun  17077  mgmidsssn0  18606  mnd1id  18714  0subm  18751  efmnd1bas  18827  smndex1basss  18839  smndex1mgm  18841  trivsubgsnd  19093  kerf1ghm  19186  ghmqusnsglem1  19219  ghmquskerlem1  19222  ghmqusker  19226  symg1bas  19328  pmtrprfvalrn  19425  gex1  19528  sylow2alem1  19554  lsmdisj2  19619  0frgp  19716  0cyg  19830  prmcyg  19831  dprddisj2  19978  ablfacrp  20005  lspdisj  21042  lidlnz  21159  mulgrhm2  21395  pzriprnglem10  21407  ocvin  21590  psrlidm  21878  mplcoe1  21951  mplcoe5  21954  psdmul  22060  maducoeval2  22534  madugsum  22537  en2top  22879  restsn  23064  ist1-3  23243  ordtt1  23273  cmpcld  23296  unisngl  23421  dissnlocfin  23423  ptopn2  23478  snfil  23758  alexsubALTlem2  23942  alexsubALTlem3  23943  alexsubALTlem4  23944  haustsms2  24031  tsmsxplem1  24047  tsmsxplem2  24048  ust0  24114  dscopn  24468  nmoid  24637  limcdif  25784  ellimc2  25785  limcmpt  25791  limcres  25794  ply1remlem  26077  plyeq0lem  26122  plyremlem  26219  aaliou2  26255  radcnv0  26332  abelthlem2  26349  wilthlem2  26986  vmappw  27033  ppinprm  27069  chtnprm  27071  musumsum  27109  dchrhash  27189  lgsquadlem1  27298  lgsquadlem2  27299  ssltsn  27711  ssltleft  27789  ssltright  27790  cofcutr  27839  addsuniflem  27915  negsid  27954  negsunif  27968  ssltmul1  28057  ssltmul2  28058  precsexlem11  28126  onscutlt  28172  n0sfincut  28253  0reno  28355  cplgr1v  29364  rusgrnumwwlkb0  29908  frgrncvvdeq  30245  fusgr2wsp2nb  30270  hsn0elch  31184  cycpmrn  33107  qsxpid  33340  prmidl0  33428  ccfldextdgrr  33674  xrge0iifiso  33932  qqhval2  33979  esumnul  34045  esumrnmpt2  34065  esumfzf  34066  sibfof  34338  sitgaddlemb  34346  plymulx0  34545  signstf0  34566  prodfzo03  34601  circlemeth  34638  sconnpi1  35233  dffr5  35748  elima4  35770  brsingle  35912  dfiota3  35918  funpartfun  35938  dfrdg4  35946  fwddifn0  36159  bj-csbsnlem  36898  bj-axsn  37027  bj-axadj  37036  bj-pw0ALT  37044  bj-restsn  37077  bj-rest10  37083  mptsnunlem  37333  fvineqsneu  37406  matunitlindflem1  37617  poimirlem23  37644  poimirlem26  37647  poimirlem27  37648  grposnOLD  37883  0idl  38026  smprngopr  38053  isdmn3  38075  ressn2  38440  lshpdisj  38987  lsat0cv  39033  snatpsubN  39751  dibelval3  41148  dib1dim  41166  dvh2dim  41446  mapd0  41666  hdmap14lem13  41881  dvrelogpow2b  42063  sticksstones11  42151  unitscyglem4  42193  sn-iotalem  42216  prjspeclsp  42607  pellexlem5  42828  jm2.23  42992  flcidc  43166  tfsconcatrn  43338  snhesn  43782  snssiALTVD  44823  snssiALT  44824  permaxinf2lem  45009  fsneq  45207  iccintsng  45528  icoiccdif  45529  limcrecl  45634  lptioo2  45636  lptioo1  45637  limcresiooub  45647  limcresioolb  45648  cnrefiisplem  45834  icccncfext  45892  dvmptfprodlem  45949  dvnprodlem3  45953  dirkercncflem2  46109  fourierdlem40  46152  fourierdlem48  46159  fourierdlem51  46162  fourierdlem62  46173  fourierdlem66  46177  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem78  46189  fourierdlem79  46190  fourierdlem93  46204  fourierdlem101  46212  fourierdlem103  46214  fourierdlem104  46215  fouriersw  46236  elaa2  46239  etransclem44  46283  rrxsnicc  46305  sge00  46381  absnsb  47032  funressnfv  47048  fsetsniunop  47054  dfdfat2  47133  tz6.12-afv  47178  tz6.12-afv2  47245  otiunsndisjX  47284  iccpartgtl  47431  iccpartgt  47432  iccpartleu  47433  iccpartgel  47434  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  bgoldbtbnd  47814  dfclnbgr6  47860  dfnbgr6  47861  stgredgiun  47961  xpsnopab  48149  mo0sn  48808  tposres0  48869  setcsnterm  49483  2arwcatlem1  49588  2arwcat  49593  setc1onsubc  49595  aacllem  49794