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

Syntax hints:   ↔ wb 208   = wceq 1562   ∈ wcel 2144  {csn 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-sn 4585

This theorem is referenced by:  rabsneq  4603  dfpr2  4605  ralsnsg  4631  rexsns  4632  ralsng  4636  disjsn  4672  snprc  4678  snssb  4743  raldifsnb  4758  difprsnss  4761  pwpw0  4773  eqsn  4789  eqsndOLD  4791  snsspw  4804  dfnfc2  4889  uni0b  4894  uni0c  4895  iunid  5020  iunsn  5025  rext  5417  moabexOLD  5428  exss  5432  otiunsndisj  5491  dffr6  5605  fconstmpt  5711  opeliunxp  5716  opeliun2xp  5717  rnep  5905  restidsing  6044  xpdifid  6155  dmsnopg  6202  sniota  6514  dfmpt3  6657  tz6.12-2  6856  nfunsn  6908  fnsnfv  6948  dffv2  6964  fsneq  7018  fsn  7119  fnasrn  7129  fnsnbg  7150  fnsnbOLD  7152  fmptsng  7154  fmptsnd  7155  fvclss  7227  eqfunresadj  7346  eusvobj2  7390  resf1extb  7917  opabex3d  7948  opabex3rd  7949  opabex3  7950  xpord2pred  8127  xpord3pred  8134  frrlem12  8280  frrlem13  8281  oarec  8533  mapdm0  8825  ixp0x  8910  snmapen  9021  xpsnen  9035  marypha2lem2  9384  elirrvOLDOLD  9549  cantnfp1lem1  9635  cantnfp1lem3  9637  djuunxp  9881  dfac5lem1  10081  dfac5lem2  10082  dfac5lem4  10084  dfac5lem4OLD  10086  fin1a2lem11  10369  axdc4lem  10414  axcclem  10416  ttukeylem7  10474  xrsupexmnf  13310  xrinfmexpnf  13311  iccid  13396  fzsn  13573  fzpr  13586  seqz  14065  hashf1  14472  pr2pwpr  14494  s3iunsndisj  14983  fsum2dlem  15799  incexc2  15870  prodsn  15994  prodsnf  15996  fprod2dlem  16012  ef0lem  16110  lcmfunsnlem2  16676  1nprm  16715  vdwapun  17012  prmodvdslcmf  17085  cshwsiun  17137  chnccat  18660  mgmidsssn0  18708  mnd1id  18816  0subm  18853  efmnd1bas  18929  smndex1basss  18944  smndex1mgm  18946  trivsubgsnd  19197  kerf1ghm  19289  ghmqusnsglem1  19322  ghmquskerlem1  19325  ghmqusker  19329  symg1bas  19433  pmtrprfvalrn  19530  gex1  19633  sylow2alem1  19659  lsmdisj2  19724  0frgp  19821  0cyg  19935  prmcyg  19936  dprddisj2  20083  ablfacrp  20110  lspdisj  21197  lidlnz  21314  mulgrhm2  21532  pzriprnglem10  21544  ocvin  21728  psrlidm  22015  mplcoe1  22092  mplcoe5  22095  psdmul  22233  maducoeval2  22702  madugsum  22705  en2top  23047  restsn  23232  ist1-3  23411  ordtt1  23441  cmpcld  23464  unisngl  23589  dissnlocfin  23591  ptopn2  23646  snfil  23926  alexsubALTlem2  24110  alexsubALTlem3  24111  alexsubALTlem4  24112  haustsms2  24199  tsmsxplem1  24215  tsmsxplem2  24216  ust0  24282  dscopn  24635  nmoid  24804  limcdif  25940  ellimc2  25941  limcmpt  25947  limcres  25950  ply1remlem  26227  plyeq0lem  26272  plyn0mulidp  26347  plyremlem  26370  aaliou2  26406  radcnv0  26481  abelthlem2  26497  wilthlem2  27135  vmappw  27182  ppinprm  27218  chtnprm  27220  musumsum  27258  dchrhash  27337  lgsquadlem1  27446  lgsquadlem2  27447  eqcuts3  27899  sltsleft  27955  sltsright  27956  cofcutr  28019  addsuniflem  28096  negsid  28136  negsunif  28150  sltmuls1  28242  sltmuls2  28243  precsexlem11  28312  oncutlt  28359  n0fincut  28450  elreno2  28590  cplgr1v  29633  rusgrnumwwlkb0  30176  frgrncvvdeq  30513  fusgr2wsp2nb  30538  hsn0elch  31453  indsn  33043  cycpmrn  33325  qsxpid  33550  prmidl0  33639  mvrvalind  33837  mplmonprod  33853  esplyfvaln  33873  esplyind  33874  ccfldextdgrr  33971  xrge0iifiso  34234  qqhval2  34281  esumnul  34347  esumrnmpt2  34367  esumfzf  34368  sibfof  34639  sitgaddlemb  34647  signstf0  34864  prodfzo03  34899  circlemeth  34936  sconnpi1  35594  dffr5  36109  elima4  36131  brsingle  36270  dfiota3  36276  funpartfun  36298  dfrdg4  36306  fwddifn0  36519  mh-infprim2bi  36912  mh-infprim3bi  36913  bj-csbsnlem  37393  bj-axsn  37522  bj-axadj  37531  bj-pw0ALT  37539  bj-restsn  37577  bj-rest10  37583  mptsnunlem  37837  fvineqsneu  37910  matunitlindflem1  38120  poimirlem23  38147  poimirlem26  38150  poimirlem27  38151  grposnOLD  38386  0idl  38529  smprngopr  38556  isdmn3  38578  dfsucmap3  38967  ressn2  39036  lshpdisj  39616  lsat0cv  39662  snatpsubN  40379  dibelval3  41776  dib1dim  41794  dvh2dim  42074  mapd0  42294  hdmap14lem13  42509  dvrelogpow2b  42690  sticksstones11  42778  unitscyglem4  42820  sn-iotalem  42845  prjspeclsp  43199  pellexlem5  43415  jm2.23  43578  flcidc  43752  tfsconcatrn  43924  snhesn  44367  snssiALTVD  45407  snssiALT  45408  permaxinf2lem  45593  iccintsng  46104  icoiccdif  46105  limcrecl  46210  lptioo2  46212  lptioo1  46213  limcresiooub  46221  limcresioolb  46222  cnrefiisplem  46408  icccncfext  46466  dvmptfprodlem  46523  dvnprodlem3  46527  dirkercncflem2  46683  fourierdlem40  46726  fourierdlem48  46733  fourierdlem51  46736  fourierdlem62  46747  fourierdlem66  46751  fourierdlem74  46759  fourierdlem75  46760  fourierdlem76  46761  fourierdlem78  46763  fourierdlem79  46764  fourierdlem93  46778  fourierdlem101  46786  fourierdlem103  46788  fourierdlem104  46789  fouriersw  46810  elaa2  46813  etransclem44  46857  rrxsnicc  46879  sge00  46955  chnsubseq  47461  absnsb  47626  funressnfv  47642  fsetsniunop  47648  dfdfat2  47727  tz6.12-afv  47772  tz6.12-afv2  47839  otiunsndisjX  47878  iccpartgtl  48037  iccpartgt  48038  iccpartleu  48039  iccpartgel  48040  nnsum4primeseven  48427  nnsum4primesevenALTV  48428  bgoldbtbnd  48436  dfclnbgr6  48483  dfnbgr6  48484  stgredgiun  48585  xpsnopab  48784  mo0sn  49442  tposres0  49503  setcsnterm  50116  2arwcatlem1  50221  2arwcat  50226  setc1onsubc  50228  aacllem  50427