Theorem velsn 4594

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113  {csn 4578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-sn 4579

This theorem is referenced by:  rabsneq  4597  dfpr2  4599  ralsnsg  4625  rexsns  4626  ralsng  4630  disjsn  4666  snprc  4672  snssb  4737  raldifsnb  4750  difprsnss  4753  pwpw0  4767  eqsn  4783  eqsndOLD  4785  snsspw  4798  dfnfc2  4883  uni0b  4887  uni0c  4888  iunid  5014  iunsn  5019  sndisj  5088  rext  5394  moabexOLD  5405  exss  5409  otiunsndisj  5466  dffr6  5578  fconstmpt  5684  opeliunxp  5689  opeliun2xp  5690  rnep  5874  restidsing  6010  xpdifid  6124  dmsnopg  6169  sniota  6481  dfmpt3  6624  tz6.12-2  6819  nfunsn  6871  fnsnfv  6911  dffv2  6927  fsn  7078  fnasrn  7088  fnsnbg  7108  fnsnbOLD  7110  fmptsng  7112  fmptsnd  7113  fvclss  7185  eqfunresadj  7304  eusvobj2  7348  resf1extb  7874  opabex3d  7907  opabex3rd  7908  opabex3  7909  xpord2pred  8085  xpord3pred  8092  frrlem12  8237  frrlem13  8238  oarec  8487  mapdm0  8777  ixp0x  8862  snmapen  8973  xpsnen  8987  marypha2lem2  9337  elirrvOLD  9501  cantnfp1lem1  9585  cantnfp1lem3  9587  djuunxp  9831  dfac5lem1  10031  dfac5lem2  10032  dfac5lem4  10034  dfac5lem4OLD  10036  fin1a2lem11  10318  axdc4lem  10363  axcclem  10365  ttukeylem7  10423  xrsupexmnf  13218  xrinfmexpnf  13219  iccid  13304  fzsn  13480  fzpr  13493  seqz  13971  hashf1  14378  pr2pwpr  14400  s3iunsndisj  14889  fsum2dlem  15691  incexc2  15759  prodsn  15883  prodsnf  15885  fprod2dlem  15901  ef0lem  15999  lcmfunsnlem2  16565  1nprm  16604  vdwapun  16900  prmodvdslcmf  16973  cshwsiun  17025  chnccat  18547  mgmidsssn0  18595  mnd1id  18703  0subm  18740  efmnd1bas  18816  smndex1basss  18828  smndex1mgm  18830  trivsubgsnd  19081  kerf1ghm  19174  ghmqusnsglem1  19207  ghmquskerlem1  19210  ghmqusker  19214  symg1bas  19318  pmtrprfvalrn  19415  gex1  19518  sylow2alem1  19544  lsmdisj2  19609  0frgp  19706  0cyg  19820  prmcyg  19821  dprddisj2  19968  ablfacrp  19995  lspdisj  21078  lidlnz  21195  mulgrhm2  21431  pzriprnglem10  21443  ocvin  21627  psrlidm  21915  mplcoe1  21990  mplcoe5  21993  psdmul  22107  maducoeval2  22582  madugsum  22585  en2top  22927  restsn  23112  ist1-3  23291  ordtt1  23321  cmpcld  23344  unisngl  23469  dissnlocfin  23471  ptopn2  23526  snfil  23806  alexsubALTlem2  23990  alexsubALTlem3  23991  alexsubALTlem4  23992  haustsms2  24079  tsmsxplem1  24095  tsmsxplem2  24096  ust0  24162  dscopn  24515  nmoid  24684  limcdif  25831  ellimc2  25832  limcmpt  25838  limcres  25841  ply1remlem  26124  plyeq0lem  26169  plyremlem  26266  aaliou2  26302  radcnv0  26379  abelthlem2  26396  wilthlem2  27033  vmappw  27080  ppinprm  27116  chtnprm  27118  musumsum  27156  dchrhash  27236  lgsquadlem1  27345  lgsquadlem2  27346  eqscut3  27792  ssltleft  27842  ssltright  27843  cofcutr  27895  addsuniflem  27971  negsid  28010  negsunif  28024  ssltmul1  28116  ssltmul2  28117  precsexlem11  28185  onscutlt  28232  n0sfincut  28315  elreno2  28440  cplgr1v  29452  rusgrnumwwlkb0  29996  frgrncvvdeq  30333  fusgr2wsp2nb  30358  hsn0elch  31272  indsn  32894  cycpmrn  33174  qsxpid  33392  prmidl0  33480  mvrvalind  33652  esplyind  33680  ccfldextdgrr  33778  xrge0iifiso  34041  qqhval2  34088  esumnul  34154  esumrnmpt2  34174  esumfzf  34175  sibfof  34446  sitgaddlemb  34454  plymulx0  34653  signstf0  34674  prodfzo03  34709  circlemeth  34746  sconnpi1  35382  dffr5  35897  elima4  35919  brsingle  36058  dfiota3  36064  funpartfun  36086  dfrdg4  36094  fwddifn0  36307  bj-csbsnlem  37047  bj-axsn  37176  bj-axadj  37185  bj-pw0ALT  37193  bj-restsn  37226  bj-rest10  37232  mptsnunlem  37482  fvineqsneu  37555  matunitlindflem1  37756  poimirlem23  37783  poimirlem26  37786  poimirlem27  37787  grposnOLD  38022  0idl  38165  smprngopr  38192  isdmn3  38214  dfsucmap3  38576  ressn2  38644  lshpdisj  39186  lsat0cv  39232  snatpsubN  39949  dibelval3  41346  dib1dim  41364  dvh2dim  41644  mapd0  41864  hdmap14lem13  42079  dvrelogpow2b  42261  sticksstones11  42349  unitscyglem4  42391  sn-iotalem  42419  prjspeclsp  42797  pellexlem5  43017  jm2.23  43180  flcidc  43354  tfsconcatrn  43526  snhesn  43969  snssiALTVD  45009  snssiALT  45010  permaxinf2lem  45195  fsneq  45392  iccintsng  45711  icoiccdif  45712  limcrecl  45817  lptioo2  45819  lptioo1  45820  limcresiooub  45828  limcresioolb  45829  cnrefiisplem  46015  icccncfext  46073  dvmptfprodlem  46130  dvnprodlem3  46134  dirkercncflem2  46290  fourierdlem40  46333  fourierdlem48  46340  fourierdlem51  46343  fourierdlem62  46354  fourierdlem66  46358  fourierdlem74  46366  fourierdlem75  46367  fourierdlem76  46368  fourierdlem78  46370  fourierdlem79  46371  fourierdlem93  46385  fourierdlem101  46393  fourierdlem103  46395  fourierdlem104  46396  fouriersw  46417  elaa2  46420  etransclem44  46464  rrxsnicc  46486  sge00  46562  chnsubseq  47066  absnsb  47215  funressnfv  47231  fsetsniunop  47237  dfdfat2  47316  tz6.12-afv  47361  tz6.12-afv2  47428  otiunsndisjX  47467  iccpartgtl  47614  iccpartgt  47615  iccpartleu  47616  iccpartgel  47617  nnsum4primeseven  47988  nnsum4primesevenALTV  47989  bgoldbtbnd  47997  dfclnbgr6  48044  dfnbgr6  48045  stgredgiun  48146  xpsnopab  48345  mo0sn  49003  tposres0  49064  setcsnterm  49677  2arwcatlem1  49782  2arwcat  49787  setc1onsubc  49789  aacllem  49988