Theorem velsn 4600

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2147  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-sn 4589

This theorem is used by:  rabsneq  4603  dfpr2  4605  ralsnsg  4631  rexsns  4632  ralsng  4636  disjsn  4672  snprc  4678  snssb  4743  raldifsnb  4759  difprsnss  4762  eqsn  4788  snsspw  4802  pwpw0  4834  dfnfc2  4892  uni0b  4897  uni0c  4898  iunid  5022  iunsn  5027  rext  5420  moabexOLD  5431  exss  5435  otiunsndisj  5497  dffr6  5611  fconstmpt  5717  opeliunxp  5722  opeliun2xp  5723  rnep  5915  restidsing  6056  xpdifid  6170  dmsnopg  6226  sniota  6546  dfmpt3  6692  tz6.12-2  6892  nfunsn  6944  fnsnfv  6984  dffv2  7000  fsneq  7054  fsn  7157  fnasrn  7169  fnsnbg  7190  fmptsng  7193  fmptsnd  7194  fvclss  7265  eqfunresadj  7390  eusvobj2  7432  resf1extb  7967  opabex3d  7998  opabex3rd  7999  opabex3  8000  xpord2pred  8186  xpord3pred  8193  frrlem12  8340  frrlem13  8341  oarec  8595  mapdm0  8887  ixp0x  8979  snmapen  9091  xpsnen  9105  marypha2lem2  9452  elirrvOLDOLD  9617  cantnfp1lem1  9703  cantnfp1lem3  9705  djuunxp  10026  dfac5lem1  10226  dfac5lem2  10227  dfac5lem4  10229  fin1a2lem11  10512  axdc4lem  10557  axcclem  10559  ttukeylem7  10617  xrsupexmnf  13459  xrinfmexpnf  13460  iccid  13545  fzsn  13724  fzpr  13737  seqz  14217  hashf1  14626  pr2pwpr  14648  s3iunsndisj  15147  fsum2dlem  15962  incexc2  16033  prodsn  16155  prodsnf  16157  fprod2dlem  16173  ef0lem  16270  lcmfunsnlem2  16841  1nprm  16880  vdwapun  17178  prmodvdslcmf  17251  cshwsiun  17303  chnccat  18826  mgmidsssn0  18879  mnd1id  19000  0subm  19039  efmnd1bas  19115  smndex1basss  19130  smndex1mgm  19132  trivsubgsnd  19390  qsxpid  19413  kerf1ghm  19487  ghmqusnsglem1  19521  ghmquskerlem1  19524  ghmqusker  19528  symg1bas  19632  pmtrprfvalrn  19729  gex1  19832  sylow2alem1  19858  lsmdisj2  19923  0frgp  20020  0cyg  20134  prmcyg  20135  dprddisj2  20282  ablfacrp  20309  lspdisj  21430  lidlnz  21557  prmidl0  21661  mulgrhm2  21811  pzriprnglem10  21823  ocvin  22007  psrlidm  22296  mplcoe1  22373  mplcoe5  22376  psdmul  22514  maducoeval2  22982  madugsum  22985  matunitlindflem1  23021  en2top  23330  restsn  23515  ist1-3  23694  ordtt1  23724  cmpcld  23747  unisngl  23873  dissnlocfin  23875  ptopn2  23930  snfil  24210  alexsubALTlem2  24394  alexsubALTlem3  24395  alexsubALTlem4  24396  haustsms2  24483  tsmsxplem1  24499  tsmsxplem2  24500  ust0  24566  dscopn  24919  nmoid  25088  limcdif  26223  ellimc2  26224  limcmpt  26230  limcres  26233  ply1remlem  26510  plyeq0lem  26556  plyn0mulidp  26629  plyremlem  26652  aaliou2  26694  radcnv0  26770  abelthlem2  26786  wilthlem2  27423  vmappw  27470  ppinprm  27506  chtnprm  27508  musumsum  27546  dchrhash  27625  lgsquadlem1  27734  lgsquadlem2  27735  eqcuts3  28217  sltsleft  28273  sltsright  28274  cofcutr  28337  addsuniflem  28414  negsid  28454  negsunif  28468  sltmuls1  28560  sltmuls2  28561  precsexlem11  28630  oncutlt  28677  n0fincut  28768  elreno2  28908  cplgr1v  30038  rusgrnumwwlkb0  30590  frgrncvvdeq  30937  fusgr2wsp2nb  30962  hsn0elch  31877  indsn  33497  cycpmrn  33771  mvrvalind  34237  mplmonprod  34253  esplyfvaln  34273  esplyind  34274  ccfldextdgrr  34371  xrge0iifiso  34634  qqhval2  34681  esumnul  34747  esumrnmpt2  34767  esumfzf  34768  sibfof  35039  sitgaddlemb  35047  signstf0  35264  prodfzo03  35299  circlemeth  35336  scottsn  35833  kard0  35921  sconnpi1  36170  elpssmo  36635  elima4  36717  brsingle  36856  dfiota3  36862  funpartfun  36884  dfrdg4  36892  fwddifn0  37106  mh-infprim2bi  37512  mh-infprim3bi  37513  bj-csbsnlem  37992  bj-axsn  38122  bj-axadj  38131  bj-pw0ALT  38154  bj-restsn  38193  bj-rest10  38199  mptsnunlem  38452  fvineqsneu  38525  poimirlem23  38752  poimirlem26  38755  poimirlem27  38756  negprop  38834  grposnOLD  39007  0idl  39150  smprngopr  39177  isdmn3  39199  dfsucmap3  39586  ressn2  39655  lshpdisj  40235  lsat0cv  40281  snatpsubN  40998  dibelval3  42395  dib1dim  42413  dvh2dim  42693  mapd0  42913  hdmap14lem13  43128  dvrelogpow2b  43309  sticksstones11  43397  unitscyglem4  43439  sn-iotalem  43466  prjspeclsp  43831  pellexlem5  44031  jm2.23  44194  flcidc  44362  tfsconcatrn  44534  snhesn  44976  snssiALTVD  45998  snssiALT  45999  permaxinf2lem  46195  iccintsng  46738  icoiccdif  46739  limcrecl  46844  lptioo2  46846  lptioo1  46847  limcresiooub  46855  limcresioolb  46856  cnrefiisplem  47042  icccncfext  47100  dvmptfprodlem  47157  dvnprodlem3  47161  dirkercncflem2  47317  fourierdlem40  47360  fourierdlem48  47367  fourierdlem51  47370  fourierdlem62  47381  fourierdlem66  47385  fourierdlem74  47393  fourierdlem75  47394  fourierdlem76  47395  fourierdlem78  47397  fourierdlem79  47398  fourierdlem93  47412  fourierdlem101  47420  fourierdlem103  47422  fourierdlem104  47423  fouriersw  47444  elaa2  47447  etransclem44  47491  rrxsnicc  47513  sge00  47589  absnsb  48300  funressnfv  48316  fsetsniunop  48322  dfdfat2  48401  tz6.12-afv  48446  tz6.12-afv2  48513  otiunsndisjX  48552  iccpartgtl  48711  iccpartgt  48712  iccpartleu  48713  iccpartgel  48714  nnsum4primeseven  49101  nnsum4primesevenALTV  49102  bgoldbtbnd  49110  dfclnbgr6  49157  dfnbgr6  49158  stgredgiun  49259  xpsnopab  49458  smprngprmrng  49639  isidom3  49645  mo0sn  50130  tposres0  50193  setcsnterm  50828  2arwcatlem1  50936  2arwcat  50941  setc1onsubc  50943  aacllem  51217