Theorem velsn 4642

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2108  {csn 4626

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-sn 4627

This theorem is referenced by:  rabsneq  4644  dfpr2  4646  ralsnsg  4670  rexsns  4671  ralsng  4675  disjsn  4711  snprc  4717  snssb  4782  snssgOLD  4784  raldifsnb  4796  difprsnss  4799  pwpw0  4813  eqsn  4829  eqsndOLD  4831  snsspw  4844  dfnfc2  4929  uni0b  4933  uni0c  4934  iunid  5060  iunsn  5066  sndisj  5135  rext  5453  moabex  5464  exss  5468  otiunsndisj  5525  dffr6  5640  fconstmpt  5747  opeliunxp  5752  opeliun2xp  5753  rnep  5937  restidsing  6071  xpdifid  6188  dmsnopg  6233  sniota  6552  dfmpt3  6702  nfunsn  6948  fnsnfv  6988  dffv2  7004  fsn  7155  fnasrn  7165  fnsnb  7186  fmptsng  7188  fmptsnd  7189  fvclss  7261  eqfunresadj  7380  eusvobj2  7423  sucexeloniOLD  7830  suceloniOLD  7832  resf1extb  7956  opabex3d  7990  opabex3rd  7991  opabex3  7992  xpord2pred  8170  xpord3pred  8177  frrlem12  8322  frrlem13  8323  wfrlem14OLD  8362  wfrlem15OLD  8363  oarec  8600  mapdm0  8882  ixp0x  8966  snmapen  9078  xpsnen  9095  marypha2lem2  9476  elirrv  9636  cantnfp1lem1  9718  cantnfp1lem3  9720  djuunxp  9961  dfac5lem1  10163  dfac5lem2  10164  dfac5lem4  10166  dfac5lem4OLD  10168  fin1a2lem11  10450  axdc4lem  10495  axcclem  10497  ttukeylem7  10555  xrsupexmnf  13347  xrinfmexpnf  13348  iccid  13432  fzsn  13606  fzpr  13619  seqz  14091  hashf1  14496  pr2pwpr  14518  s3iunsndisj  15007  fsum2dlem  15806  incexc2  15874  prodsn  15998  prodsnf  16000  fprod2dlem  16016  ef0lem  16114  lcmfunsnlem2  16677  1nprm  16716  vdwapun  17012  prmodvdslcmf  17085  cshwsiun  17137  mgmidsssn0  18685  mnd1id  18793  0subm  18830  efmnd1bas  18906  smndex1basss  18918  smndex1mgm  18920  trivsubgsnd  19172  kerf1ghm  19265  ghmqusnsglem1  19298  ghmquskerlem1  19301  ghmqusker  19305  symg1bas  19408  pmtrprfvalrn  19506  gex1  19609  sylow2alem1  19635  lsmdisj2  19700  0frgp  19797  0cyg  19911  prmcyg  19912  dprddisj2  20059  ablfacrp  20086  lspdisj  21127  lidlnz  21252  mulgrhm2  21489  pzriprnglem10  21501  ocvin  21692  psrlidm  21982  mplcoe1  22055  mplcoe5  22058  psdmul  22170  maducoeval2  22646  madugsum  22649  en2top  22992  restsn  23178  ist1-3  23357  ordtt1  23387  cmpcld  23410  unisngl  23535  dissnlocfin  23537  ptopn2  23592  snfil  23872  alexsubALTlem2  24056  alexsubALTlem3  24057  alexsubALTlem4  24058  haustsms2  24145  tsmsxplem1  24161  tsmsxplem2  24162  ust0  24228  dscopn  24586  nmoid  24763  limcdif  25911  ellimc2  25912  limcmpt  25918  limcres  25921  ply1remlem  26204  plyeq0lem  26249  plyremlem  26346  aaliou2  26382  radcnv0  26459  abelthlem2  26476  wilthlem2  27112  vmappw  27159  ppinprm  27195  chtnprm  27197  musumsum  27235  dchrhash  27315  lgsquadlem1  27424  lgsquadlem2  27425  ssltsn  27837  ssltleft  27909  ssltright  27910  cofcutr  27958  addsuniflem  28034  negsid  28073  negsunif  28087  ssltmul1  28173  ssltmul2  28174  precsexlem11  28241  nohalf  28407  0reno  28429  cplgr1v  29447  rusgrnumwwlkb0  29991  frgrncvvdeq  30328  fusgr2wsp2nb  30353  hsn0elch  31267  cycpmrn  33163  qsxpid  33390  prmidl0  33478  ccfldextdgrr  33722  xrge0iifiso  33934  qqhval2  33983  esumnul  34049  esumrnmpt2  34069  esumfzf  34070  sibfof  34342  sitgaddlemb  34350  plymulx0  34562  signstf0  34583  prodfzo03  34618  circlemeth  34655  sconnpi1  35244  dffr5  35754  elima4  35776  brsingle  35918  dfiota3  35924  funpartfun  35944  dfrdg4  35952  fwddifn0  36165  bj-csbsnlem  36904  bj-axsn  37033  bj-axadj  37042  bj-pw0ALT  37050  bj-restsn  37083  bj-rest10  37089  mptsnunlem  37339  fvineqsneu  37412  matunitlindflem1  37623  poimirlem23  37650  poimirlem26  37653  poimirlem27  37654  grposnOLD  37889  0idl  38032  smprngopr  38059  isdmn3  38081  ressn2  38443  lshpdisj  38988  lsat0cv  39034  snatpsubN  39752  dibelval3  41149  dib1dim  41167  dvh2dim  41447  mapd0  41667  hdmap14lem13  41882  dvrelogpow2b  42069  sticksstones11  42157  unitscyglem4  42199  sn-iotalem  42260  fnsnbt  42271  prjspeclsp  42622  pellexlem5  42844  jm2.23  43008  flcidc  43182  tfsconcatrn  43355  snhesn  43799  snssiALTVD  44847  snssiALT  44848  fsneq  45211  iccintsng  45536  icoiccdif  45537  limcrecl  45644  lptioo2  45646  lptioo1  45647  limcresiooub  45657  limcresioolb  45658  cnrefiisplem  45844  icccncfext  45902  dvmptfprodlem  45959  dvnprodlem3  45963  dirkercncflem2  46119  fourierdlem40  46162  fourierdlem48  46169  fourierdlem51  46172  fourierdlem62  46183  fourierdlem66  46187  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem78  46199  fourierdlem79  46200  fourierdlem93  46214  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  fouriersw  46246  elaa2  46249  etransclem44  46293  rrxsnicc  46315  sge00  46391  absnsb  47039  funressnfv  47055  fsetsniunop  47061  dfdfat2  47140  tz6.12-afv  47185  tz6.12-afv2  47252  otiunsndisjX  47291  iccpartgtl  47413  iccpartgt  47414  iccpartleu  47415  iccpartgel  47416  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  bgoldbtbnd  47796  dfclnbgr6  47842  dfnbgr6  47843  stgredgiun  47925  xpsnopab  48073  mo0sn  48735  tposres0  48777  setcsnterm  49133  aacllem  49320