Theorem velsn 4585

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

Syntax hints:   ↔ wb 208   = wceq 1537   ∈ wcel 2114  {csn 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-sn 4570

This theorem is referenced by:  dfpr2  4588  ralsnsg  4610  rexsns  4611  disjsn  4649  snprc  4655  snssg  4719  raldifsnb  4731  difprsnss  4734  pwpw0  4748  eqsn  4764  snsspw  4777  pwsnOLD  4833  dfnfc2  4862  uni0b  4866  uni0c  4867  sndisj  5059  rext  5343  moabex  5353  exss  5357  otiunsndisj  5412  fconstmpt  5616  opeliunxp  5621  rnep  5799  restidsing  5924  xpdifid  6027  dmsnopg  6072  sniota  6348  dfmpt3  6484  nfunsn  6709  dffv2  6758  fsn  6899  fnasrn  6909  fnsnb  6930  fmptsng  6932  fmptsnd  6933  fvclss  7003  eusvobj2  7151  suceloni  7530  opabex3d  7668  opabex3rd  7669  opabex3  7670  wfrlem14  7970  wfrlem15  7971  oarec  8190  mapdm0  8423  ixp0x  8492  snmapen  8592  xpsnen  8603  marypha2lem2  8902  elirrv  9062  cantnfp1lem1  9143  cantnfp1lem3  9145  djuunxp  9352  dfac5lem1  9551  dfac5lem2  9552  dfac5lem4  9554  fin1a2lem11  9834  axdc4lem  9879  axcclem  9881  ttukeylem7  9939  xrsupexmnf  12701  xrinfmexpnf  12702  iccid  12786  fzsn  12952  fzpr  12965  seqz  13421  hashf1  13818  pr2pwpr  13840  s3iunsndisj  14330  fsum2dlem  15127  incexc2  15195  prodsn  15318  prodsnf  15320  fprod2dlem  15336  ef0lem  15434  lcmfunsnlem2  15986  1nprm  16025  vdwapun  16312  prmodvdslcmf  16385  cshwsiun  16435  mgmidsssn0  17884  mnd1id  17955  0subm  17984  efmnd1bas  18060  smndex1basss  18072  smndex1mgm  18074  trivsubgsnd  18308  symg1bas  18521  pmtrprfvalrn  18618  gex1  18718  sylow2alem1  18744  lsmdisj2  18810  0frgp  18907  0cyg  19015  prmcyg  19016  dprddisj2  19163  ablfacrp  19190  kerf1ghm  19499  kerf1hrmOLD  19500  lspdisj  19899  lidlnz  20003  psrlidm  20185  mplcoe1  20248  mplcoe5  20251  mulgrhm2  20648  ocvin  20820  maducoeval2  21251  madugsum  21254  en2top  21595  restsn  21780  ist1-3  21959  ordtt1  21989  cmpcld  22012  unisngl  22137  dissnlocfin  22139  ptopn2  22194  snfil  22474  alexsubALTlem2  22658  alexsubALTlem3  22659  alexsubALTlem4  22660  haustsms2  22747  tsmsxplem1  22763  tsmsxplem2  22764  ust0  22830  dscopn  23185  nmoid  23353  limcdif  24476  ellimc2  24477  limcmpt  24483  limcres  24486  ply1remlem  24758  plyeq0lem  24802  plyremlem  24895  aaliou2  24931  radcnv0  25006  abelthlem2  25022  wilthlem2  25648  vmappw  25695  ppinprm  25731  chtnprm  25733  musumsum  25771  dchrhash  25849  lgsquadlem1  25958  lgsquadlem2  25959  cplgr1v  27214  rusgrnumwwlkb0  27752  frgrncvvdeq  28090  fusgr2wsp2nb  28115  hsn0elch  29027  eqsnd  30291  cycpmrn  30787  qsxpid  30929  ccfldextdgrr  31059  xrge0iifiso  31180  qqhval2  31225  esumnul  31309  esumrnmpt2  31329  esumfzf  31330  sibfof  31600  sitgaddlemb  31608  plymulx0  31819  signstf0  31840  prodfzo03  31876  circlemeth  31913  bnj521  32009  sconnpi1  32488  dffr5  32991  eqfunresadj  33006  elima4  33021  frrlem12  33136  frrlem13  33137  brsingle  33380  dfiota3  33386  funpartfun  33406  dfrdg4  33414  fwddifn0  33627  bj-csbsnlem  34222  bj-pw0ALT  34344  bj-restsn  34375  bj-rest10  34381  mptsnunlem  34621  fvineqsneu  34694  matunitlindflem1  34890  poimirlem23  34917  poimirlem26  34920  poimirlem27  34921  grposnOLD  35162  0idl  35305  smprngopr  35332  isdmn3  35354  lshpdisj  36125  lsat0cv  36171  snatpsubN  36888  dibelval3  38285  dib1dim  38303  dvh2dim  38583  mapd0  38803  hdmap14lem13  39018  iunsn  39125  fnsnbt  39127  prjspeclsp  39269  pellexlem5  39437  jm2.23  39600  flcidc  39781  snhesn  40139  snssiALTVD  41168  snssiALT  41169  fsneq  41476  iccintsng  41806  icoiccdif  41807  limcrecl  41917  lptioo2  41919  lptioo1  41920  limcresiooub  41930  limcresioolb  41931  cnrefiisplem  42117  icccncfext  42177  dvmptfprodlem  42236  dvnprodlem3  42240  dirkercncflem2  42396  fourierdlem40  42439  fourierdlem48  42446  fourierdlem51  42449  fourierdlem62  42460  fourierdlem66  42464  fourierdlem74  42472  fourierdlem75  42473  fourierdlem76  42474  fourierdlem78  42476  fourierdlem79  42477  fourierdlem93  42491  fourierdlem101  42499  fourierdlem103  42501  fourierdlem104  42502  fouriersw  42523  elaa2  42526  etransclem44  42570  rrxsnicc  42592  sge00  42665  absnsb  43269  funressnfv  43285  dfdfat2  43334  tz6.12-afv  43379  tz6.12-afv2  43446  otiunsndisjX  43485  iccpartgtl  43593  iccpartgt  43594  iccpartleu  43595  iccpartgel  43596  nnsum4primeseven  43972  nnsum4primesevenALTV  43973  bgoldbtbnd  43981  xpsnopab  44039  opeliun2xp  44388  aacllem  44909