Theorem velsn 4583

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-sn 4568

This theorem is referenced by:  rabsneq  4586  dfpr2  4588  ralsnsg  4614  rexsns  4615  ralsng  4619  disjsn  4655  snprc  4661  snssb  4726  raldifsnb  4741  difprsnss  4744  pwpw0  4756  eqsn  4772  eqsndOLD  4774  snsspw  4787  dfnfc2  4872  uni0b  4876  uni0c  4877  iunid  5003  iunsn  5008  rext  5400  moabexOLD  5411  exss  5415  otiunsndisj  5474  dffr6  5587  fconstmpt  5693  opeliunxp  5698  opeliun2xp  5699  rnep  5882  restidsing  6018  xpdifid  6132  dmsnopg  6177  sniota  6489  dfmpt3  6632  tz6.12-2  6827  nfunsn  6879  fnsnfv  6919  dffv2  6935  fsn  7088  fnasrn  7098  fnsnbg  7119  fnsnbOLD  7121  fmptsng  7123  fmptsnd  7124  fvclss  7196  eqfunresadj  7315  eusvobj2  7359  resf1extb  7885  opabex3d  7918  opabex3rd  7919  opabex3  7920  xpord2pred  8095  xpord3pred  8102  frrlem12  8247  frrlem13  8248  oarec  8497  mapdm0  8789  ixp0x  8874  snmapen  8985  xpsnen  8999  marypha2lem2  9349  elirrvOLD  9513  cantnfp1lem1  9599  cantnfp1lem3  9601  djuunxp  9845  dfac5lem1  10045  dfac5lem2  10046  dfac5lem4  10048  dfac5lem4OLD  10050  fin1a2lem11  10332  axdc4lem  10377  axcclem  10379  ttukeylem7  10437  xrsupexmnf  13257  xrinfmexpnf  13258  iccid  13343  fzsn  13520  fzpr  13533  seqz  14012  hashf1  14419  pr2pwpr  14441  s3iunsndisj  14930  fsum2dlem  15732  incexc2  15803  prodsn  15927  prodsnf  15929  fprod2dlem  15945  ef0lem  16043  lcmfunsnlem2  16609  1nprm  16648  vdwapun  16945  prmodvdslcmf  17018  cshwsiun  17070  chnccat  18592  mgmidsssn0  18640  mnd1id  18748  0subm  18785  efmnd1bas  18861  smndex1basss  18876  smndex1mgm  18878  trivsubgsnd  19129  kerf1ghm  19222  ghmqusnsglem1  19255  ghmquskerlem1  19258  ghmqusker  19262  symg1bas  19366  pmtrprfvalrn  19463  gex1  19566  sylow2alem1  19592  lsmdisj2  19657  0frgp  19754  0cyg  19868  prmcyg  19869  dprddisj2  20016  ablfacrp  20043  lspdisj  21123  lidlnz  21240  mulgrhm2  21458  pzriprnglem10  21470  ocvin  21654  psrlidm  21940  mplcoe1  22015  mplcoe5  22018  psdmul  22132  maducoeval2  22605  madugsum  22608  en2top  22950  restsn  23135  ist1-3  23314  ordtt1  23344  cmpcld  23367  unisngl  23492  dissnlocfin  23494  ptopn2  23549  snfil  23829  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALTlem4  24015  haustsms2  24102  tsmsxplem1  24118  tsmsxplem2  24119  ust0  24185  dscopn  24538  nmoid  24707  limcdif  25843  ellimc2  25844  limcmpt  25850  limcres  25853  ply1remlem  26130  plyeq0lem  26175  plyremlem  26270  aaliou2  26306  radcnv0  26381  abelthlem2  26397  wilthlem2  27032  vmappw  27079  ppinprm  27115  chtnprm  27117  musumsum  27155  dchrhash  27234  lgsquadlem1  27343  lgsquadlem2  27344  eqcuts3  27796  sltsleft  27852  sltsright  27853  cofcutr  27916  addsuniflem  27993  negsid  28033  negsunif  28047  sltmuls1  28139  sltmuls2  28140  precsexlem11  28209  oncutlt  28256  n0fincut  28347  elreno2  28487  cplgr1v  29499  rusgrnumwwlkb0  30042  frgrncvvdeq  30379  fusgr2wsp2nb  30404  hsn0elch  31319  indsn  32923  cycpmrn  33204  qsxpid  33422  prmidl0  33510  mvrvalind  33682  mplmonprod  33698  esplyfvaln  33718  esplyind  33719  ccfldextdgrr  33816  xrge0iifiso  34079  qqhval2  34126  esumnul  34192  esumrnmpt2  34212  esumfzf  34213  sibfof  34484  sitgaddlemb  34492  plymulx0  34691  signstf0  34712  prodfzo03  34747  circlemeth  34784  sconnpi1  35421  dffr5  35936  elima4  35958  brsingle  36097  dfiota3  36103  funpartfun  36125  dfrdg4  36133  fwddifn0  36346  mh-infprim2bi  36729  mh-infprim3bi  36730  bj-csbsnlem  37210  bj-axsn  37339  bj-axadj  37348  bj-pw0ALT  37356  bj-restsn  37394  bj-rest10  37400  mptsnunlem  37654  fvineqsneu  37727  matunitlindflem1  37937  poimirlem23  37964  poimirlem26  37967  poimirlem27  37968  grposnOLD  38203  0idl  38346  smprngopr  38373  isdmn3  38395  dfsucmap3  38784  ressn2  38853  lshpdisj  39433  lsat0cv  39479  snatpsubN  40196  dibelval3  41593  dib1dim  41611  dvh2dim  41891  mapd0  42111  hdmap14lem13  42326  dvrelogpow2b  42507  sticksstones11  42595  unitscyglem4  42637  sn-iotalem  42662  prjspeclsp  43045  pellexlem5  43261  jm2.23  43424  flcidc  43598  tfsconcatrn  43770  snhesn  44213  snssiALTVD  45253  snssiALT  45254  permaxinf2lem  45439  fsneq  45635  iccintsng  45953  icoiccdif  45954  limcrecl  46059  lptioo2  46061  lptioo1  46062  limcresiooub  46070  limcresioolb  46071  cnrefiisplem  46257  icccncfext  46315  dvmptfprodlem  46372  dvnprodlem3  46376  dirkercncflem2  46532  fourierdlem40  46575  fourierdlem48  46582  fourierdlem51  46585  fourierdlem62  46596  fourierdlem66  46600  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem78  46612  fourierdlem79  46613  fourierdlem93  46627  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fouriersw  46659  elaa2  46662  etransclem44  46706  rrxsnicc  46728  sge00  46804  chnsubseq  47310  absnsb  47475  funressnfv  47491  fsetsniunop  47497  dfdfat2  47576  tz6.12-afv  47621  tz6.12-afv2  47688  otiunsndisjX  47727  iccpartgtl  47886  iccpartgt  47887  iccpartleu  47888  iccpartgel  47889  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  bgoldbtbnd  48285  dfclnbgr6  48332  dfnbgr6  48333  stgredgiun  48434  xpsnopab  48633  mo0sn  49291  tposres0  49352  setcsnterm  49965  2arwcatlem1  50070  2arwcat  50075  setc1onsubc  50077  aacllem  50276