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

Syntax hints:   ↔ wb 205   = wceq 1542   ∈ wcel 2110  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-sn 4568

This theorem is referenced by:  dfpr2  4586  ralsnsg  4610  rexsns  4611  ralsng  4615  disjsn  4653  snprc  4659  snssg  4724  raldifsnb  4735  difprsnss  4738  pwpw0  4752  eqsn  4768  snsspw  4781  pwsnOLD  4838  dfnfc2  4869  uni0b  4873  uni0c  4874  iunsn  5000  sndisj  5070  rext  5367  moabex  5377  exss  5381  otiunsndisj  5437  dffr6  5547  fconstmpt  5649  opeliunxp  5654  rnep  5834  restidsing  5960  xpdifid  6069  dmsnopg  6114  sniota  6422  dfmpt3  6564  nfunsn  6806  fnsnfv  6842  dffv2  6858  fsn  7002  fnasrn  7012  fnsnb  7033  fmptsng  7035  fmptsnd  7036  fvclss  7110  eusvobj2  7262  suceloni  7649  opabex3d  7795  opabex3rd  7796  opabex3  7797  frrlem12  8098  frrlem13  8099  wfrlem14OLD  8138  wfrlem15OLD  8139  oarec  8370  mapdm0  8605  ixp0x  8689  snmapen  8803  xpsnen  8817  marypha2lem2  9165  elirrv  9325  cantnfp1lem1  9406  cantnfp1lem3  9408  djuunxp  9672  dfac5lem1  9872  dfac5lem2  9873  dfac5lem4  9875  fin1a2lem11  10159  axdc4lem  10204  axcclem  10206  ttukeylem7  10264  xrsupexmnf  13030  xrinfmexpnf  13031  iccid  13115  fzsn  13289  fzpr  13302  seqz  13761  hashf1  14161  pr2pwpr  14183  s3iunsndisj  14669  fsum2dlem  15472  incexc2  15540  prodsn  15662  prodsnf  15664  fprod2dlem  15680  ef0lem  15778  lcmfunsnlem2  16335  1nprm  16374  vdwapun  16665  prmodvdslcmf  16738  cshwsiun  16791  mgmidsssn0  18346  mnd1id  18417  0subm  18446  efmnd1bas  18522  smndex1basss  18534  smndex1mgm  18536  trivsubgsnd  18772  symg1bas  18988  pmtrprfvalrn  19086  gex1  19186  sylow2alem1  19212  lsmdisj2  19278  0frgp  19375  0cyg  19484  prmcyg  19485  dprddisj2  19632  ablfacrp  19659  kerf1ghm  19977  lspdisj  20377  lidlnz  20489  mulgrhm2  20690  ocvin  20869  psrlidm  21162  mplcoe1  21228  mplcoe5  21231  maducoeval2  21779  madugsum  21782  en2top  22125  restsn  22311  ist1-3  22490  ordtt1  22520  cmpcld  22543  unisngl  22668  dissnlocfin  22670  ptopn2  22725  snfil  23005  alexsubALTlem2  23189  alexsubALTlem3  23190  alexsubALTlem4  23191  haustsms2  23278  tsmsxplem1  23294  tsmsxplem2  23295  ust0  23361  dscopn  23719  nmoid  23896  limcdif  25030  ellimc2  25031  limcmpt  25037  limcres  25040  ply1remlem  25317  plyeq0lem  25361  plyremlem  25454  aaliou2  25490  radcnv0  25565  abelthlem2  25581  wilthlem2  26208  vmappw  26255  ppinprm  26291  chtnprm  26293  musumsum  26331  dchrhash  26409  lgsquadlem1  26518  lgsquadlem2  26519  cplgr1v  27787  rusgrnumwwlkb0  28324  frgrncvvdeq  28661  fusgr2wsp2nb  28686  hsn0elch  29598  eqsnd  30865  cycpmrn  31398  qsxpid  31546  prmidl0  31614  ccfldextdgrr  31730  xrge0iifiso  31873  qqhval2  31920  esumnul  32004  esumrnmpt2  32024  esumfzf  32025  sibfof  32295  sitgaddlemb  32303  plymulx0  32514  signstf0  32535  prodfzo03  32571  circlemeth  32608  bnj521  32704  sconnpi1  33189  dffr5  33709  eqfunresadj  33723  elima4  33738  xpord2pred  33780  xpord3pred  33786  ssltleft  34042  ssltright  34043  cofcutr  34080  brsingle  34207  dfiota3  34213  funpartfun  34233  dfrdg4  34241  fwddifn0  34454  bj-csbsnlem  35076  bj-pw0ALT  35210  bj-restsn  35241  bj-rest10  35247  mptsnunlem  35497  fvineqsneu  35570  matunitlindflem1  35761  poimirlem23  35788  poimirlem26  35791  poimirlem27  35792  grposnOLD  36028  0idl  36171  smprngopr  36198  isdmn3  36220  lshpdisj  36989  lsat0cv  37035  snatpsubN  37752  dibelval3  39149  dib1dim  39167  dvh2dim  39447  mapd0  39667  hdmap14lem13  39882  dvrelogpow2b  40065  sticksstones11  40101  sn-iotalem  40178  fnsnbt  40197  prjspeclsp  40440  prjcrv0  40459  pellexlem5  40644  jm2.23  40807  flcidc  40988  snhesn  41356  snssiALTVD  42409  snssiALT  42410  fsneq  42708  iccintsng  43024  icoiccdif  43025  limcrecl  43133  lptioo2  43135  lptioo1  43136  limcresiooub  43146  limcresioolb  43147  cnrefiisplem  43333  icccncfext  43391  dvmptfprodlem  43448  dvnprodlem3  43452  dirkercncflem2  43608  fourierdlem40  43651  fourierdlem48  43658  fourierdlem51  43661  fourierdlem62  43672  fourierdlem66  43676  fourierdlem74  43684  fourierdlem75  43685  fourierdlem76  43686  fourierdlem78  43688  fourierdlem79  43689  fourierdlem93  43703  fourierdlem101  43711  fourierdlem103  43713  fourierdlem104  43714  fouriersw  43735  elaa2  43738  etransclem44  43782  rrxsnicc  43804  sge00  43877  absnsb  44481  funressnfv  44497  fsetsniunop  44503  dfdfat2  44580  tz6.12-afv  44625  tz6.12-afv2  44692  otiunsndisjX  44731  iccpartgtl  44839  iccpartgt  44840  iccpartleu  44841  iccpartgel  44842  nnsum4primeseven  45213  nnsum4primesevenALTV  45214  bgoldbtbnd  45222  xpsnopab  45280  opeliun2xp  45629  mo0sn  46122  aacllem  46466