Theorem velsn 4648

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

Syntax hints:   ↔ wb 205   = wceq 1533   ∈ wcel 2098  {csn 4632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-sn 4633

This theorem is referenced by:  rabsneq  4650  dfpr2  4652  ralsnsg  4676  rexsns  4677  ralsng  4681  disjsn  4719  snprc  4725  snssb  4790  snssgOLD  4792  raldifsnb  4804  difprsnss  4807  pwpw0  4821  eqsn  4837  snsspw  4850  dfnfc2  4936  uni0b  4940  uni0c  4941  iunid  5067  iunsn  5073  sndisj  5143  rext  5453  moabex  5464  exss  5468  otiunsndisj  5525  dffr6  5639  fconstmpt  5743  opeliunxp  5748  rnep  5932  restidsing  6061  xpdifid  6178  dmsnopg  6223  sniota  6544  dfmpt3  6694  nfunsn  6942  fnsnfv  6980  dffv2  6996  fsn  7148  fnasrn  7158  fnsnb  7179  fmptsng  7181  fmptsnd  7182  fvclss  7255  eqfunresadj  7371  eusvobj2  7415  sucexeloniOLD  7818  suceloniOLD  7820  opabex3d  7978  opabex3rd  7979  opabex3  7980  xpord2pred  8158  xpord3pred  8165  frrlem12  8311  frrlem13  8312  wfrlem14OLD  8351  wfrlem15OLD  8352  oarec  8591  mapdm0  8870  ixp0x  8954  snmapen  9073  xpsnen  9092  marypha2lem2  9475  elirrv  9635  cantnfp1lem1  9717  cantnfp1lem3  9719  djuunxp  9960  dfac5lem1  10162  dfac5lem2  10163  dfac5lem4  10165  fin1a2lem11  10449  axdc4lem  10494  axcclem  10496  ttukeylem7  10554  xrsupexmnf  13333  xrinfmexpnf  13334  iccid  13418  fzsn  13592  fzpr  13605  seqz  14065  hashf1  14471  pr2pwpr  14493  s3iunsndisj  14968  fsum2dlem  15769  incexc2  15837  prodsn  15959  prodsnf  15961  fprod2dlem  15977  ef0lem  16075  lcmfunsnlem2  16636  1nprm  16675  vdwapun  16971  prmodvdslcmf  17044  cshwsiun  17097  mgmidsssn0  18660  mnd1id  18765  0subm  18802  efmnd1bas  18878  smndex1basss  18890  smndex1mgm  18892  trivsubgsnd  19143  kerf1ghm  19236  ghmqusnsglem1  19269  ghmquskerlem1  19272  ghmqusker  19276  symg1bas  19383  pmtrprfvalrn  19481  gex1  19584  sylow2alem1  19610  lsmdisj2  19675  0frgp  19772  0cyg  19886  prmcyg  19887  dprddisj2  20034  ablfacrp  20061  lspdisj  21053  lidlnz  21178  mulgrhm2  21460  pzriprnglem10  21472  ocvin  21662  psrlidm  21963  mplcoe1  22036  mplcoe5  22039  psdmul  22152  maducoeval2  22625  madugsum  22628  en2top  22971  restsn  23157  ist1-3  23336  ordtt1  23366  cmpcld  23389  unisngl  23514  dissnlocfin  23516  ptopn2  23571  snfil  23851  alexsubALTlem2  24035  alexsubALTlem3  24036  alexsubALTlem4  24037  haustsms2  24124  tsmsxplem1  24140  tsmsxplem2  24141  ust0  24207  dscopn  24565  nmoid  24742  limcdif  25888  ellimc2  25889  limcmpt  25895  limcres  25898  ply1remlem  26184  plyeq0lem  26229  plyremlem  26324  aaliou2  26360  radcnv0  26437  abelthlem2  26454  wilthlem2  27089  vmappw  27136  ppinprm  27172  chtnprm  27174  musumsum  27212  dchrhash  27292  lgsquadlem1  27401  lgsquadlem2  27402  ssltsn  27814  ssltleft  27886  ssltright  27887  cofcutr  27933  addsuniflem  28007  negsid  28042  negsunif  28056  ssltmul1  28140  ssltmul2  28141  precsexlem11  28208  0reno  28340  cplgr1v  29358  rusgrnumwwlkb0  29897  frgrncvvdeq  30234  fusgr2wsp2nb  30259  hsn0elch  31173  eqsnd  32446  cycpmrn  32998  qsxpid  33214  prmidl0  33302  ccfldextdgrr  33529  xrge0iifiso  33706  qqhval2  33753  esumnul  33837  esumrnmpt2  33857  esumfzf  33858  sibfof  34130  sitgaddlemb  34138  plymulx0  34349  signstf0  34370  prodfzo03  34405  circlemeth  34442  sconnpi1  35019  dffr5  35524  elima4  35547  brsingle  35689  dfiota3  35695  funpartfun  35715  dfrdg4  35723  fwddifn0  35936  bj-csbsnlem  36557  bj-axsn  36687  bj-axadj  36696  bj-pw0ALT  36704  bj-restsn  36737  bj-rest10  36743  mptsnunlem  36993  fvineqsneu  37066  matunitlindflem1  37265  poimirlem23  37292  poimirlem26  37295  poimirlem27  37296  grposnOLD  37531  0idl  37674  smprngopr  37701  isdmn3  37723  ressn2  38088  lshpdisj  38633  lsat0cv  38679  snatpsubN  39397  dibelval3  40794  dib1dim  40812  dvh2dim  41092  mapd0  41312  hdmap14lem13  41527  dvrelogpow2b  41715  sticksstones11  41802  sn-iotalem  41886  fnsnbt  41897  prjspeclsp  42203  pellexlem5  42427  jm2.23  42591  flcidc  42772  tfsconcatrn  42945  snhesn  43390  snssiALTVD  44440  snssiALT  44441  fsneq  44750  iccintsng  45078  icoiccdif  45079  limcrecl  45187  lptioo2  45189  lptioo1  45190  limcresiooub  45200  limcresioolb  45201  cnrefiisplem  45387  icccncfext  45445  dvmptfprodlem  45502  dvnprodlem3  45506  dirkercncflem2  45662  fourierdlem40  45705  fourierdlem48  45712  fourierdlem51  45715  fourierdlem62  45726  fourierdlem66  45730  fourierdlem74  45738  fourierdlem75  45739  fourierdlem76  45740  fourierdlem78  45742  fourierdlem79  45743  fourierdlem93  45757  fourierdlem101  45765  fourierdlem103  45767  fourierdlem104  45768  fouriersw  45789  elaa2  45792  etransclem44  45836  rrxsnicc  45858  sge00  45934  absnsb  46579  funressnfv  46595  fsetsniunop  46601  dfdfat2  46678  tz6.12-afv  46723  tz6.12-afv2  46790  otiunsndisjX  46829  iccpartgtl  46935  iccpartgt  46936  iccpartleu  46937  iccpartgel  46938  nnsum4primeseven  47309  nnsum4primesevenALTV  47310  bgoldbtbnd  47318  dfclnbgr6  47360  dfnbgr6  47361  xpsnopab  47471  opeliun2xp  47648  mo0sn  48138  aacllem  48486