Theorem velsn 4386

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

Syntax hints:   ↔ wb 197   = wceq 1637   ∈ wcel 2156  {csn 4370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-sn 4371

This theorem is referenced by:  dfpr2  4389  ralsnsg  4409  rexsns  4410  disjsn  4438  snprc  4444  euabsn2  4451  snssg  4505  raldifsnb  4517  difprsnss  4520  pwpw0  4534  eqsn  4550  snsspw  4563  pwsnALT  4623  dfnfc2  4650  uni0b  4657  uni0c  4658  sndisj  4836  rext  5106  moabex  5117  exss  5121  otiunsndisj  5175  fconstmpt  5363  opeliunxp  5370  restidsing  5670  xpdifid  5773  dmsnopg  5818  sniota  6091  dfmpt3  6225  nfunsn  6445  dffv2  6492  fsn  6625  fnasrn  6634  fnsnb  6657  fmptsng  6659  fmptsnd  6660  fvclss  6724  eusvobj2  6867  suceloni  7243  opabex3d  7375  opabex3  7376  wfrlem14  7664  wfrlem15  7665  oarec  7879  ixp0x  8173  snmapen  8273  xpsnen  8283  marypha2lem2  8581  elirrv  8740  cantnfp1lem1  8822  cantnfp1lem3  8824  djuunxp  9030  dfac5lem1  9229  dfac5lem2  9230  dfac5lem4  9232  fin1a2lem11  9517  axdc4lem  9562  axcclem  9564  ttukeylem7  9622  xrsupexmnf  12353  xrinfmexpnf  12354  iccid  12438  fzsn  12606  fzpr  12619  seqz  13072  hashf1  13458  pr2pwpr  13478  s3iunsndisj  13932  fsum2dlem  14724  incexc2  14792  prodsn  14913  prodsnf  14915  fprod2dlem  14931  ef0lem  15029  lcmfunsnlem2  15572  1nprm  15610  vdwapun  15895  prmodvdslcmf  15968  cshwsiun  16018  xpsc0  16425  xpsc1  16426  mgmidsssn0  17474  mnd1id  17537  symg1bas  18017  pmtrprfvalrn  18109  gex1  18207  sylow2alem1  18233  lsmdisj2  18296  0frgp  18393  0cyg  18495  prmcyg  18496  dprddisj2  18640  ablfacrp  18667  kerf1hrm  18947  lspdisj  19332  lidlnz  19437  psrlidm  19612  mplcoe1  19674  mplcoe5  19677  evlslem1  19723  mulgrhm2  20055  ocvin  20228  maducoeval2  20657  madugsum  20660  en2top  21003  restsn  21188  ist1-3  21367  ordtt1  21397  cmpcld  21419  unisngl  21544  dissnlocfin  21546  ptopn2  21601  snfil  21881  alexsubALTlem2  22065  alexsubALTlem3  22066  alexsubALTlem4  22067  haustsms2  22153  tsmsxplem1  22169  tsmsxplem2  22170  ust0  22236  dscopn  22591  nmoid  22759  limcdif  23854  ellimc2  23855  limcmpt  23861  limcres  23864  ply1remlem  24136  plyeq0lem  24180  plyremlem  24273  aaliou2  24309  radcnv0  24384  abelthlem2  24400  wilthlem2  25009  vmappw  25056  ppinprm  25092  chtnprm  25094  musumsum  25132  dchrhash  25210  lgsquadlem1  25319  lgsquadlem2  25320  cplgr1v  26554  rusgrnumwwlkb0  27113  frgrncvvdeq  27484  fusgr2wsp2nb  27509  hsn0elch  28433  xrge0iifiso  30306  qqhval2  30351  esumnul  30435  esumrnmpt2  30455  esumfzf  30456  sibfof  30727  sitgaddlemb  30735  plymulx0  30949  signstf0  30970  signstfvneq0  30974  prodfzo03  31006  circlemeth  31043  bnj521  31128  sconnpi1  31544  dffr5  31965  eqfunresadj  31981  elima4  31999  brsingle  32345  dfiota3  32351  funpartfun  32371  dfrdg4  32379  fwddifn0  32592  bj-csbsnlem  33206  bj-restsn  33346  bj-rest10  33352  bj-raldifsn  33365  mptsnunlem  33502  matunitlindflem1  33718  poimirlem23  33745  poimirlem26  33748  poimirlem27  33749  grposnOLD  33992  0idl  34135  smprngopr  34162  isdmn3  34184  lshpdisj  34767  lsat0cv  34813  snatpsubN  35530  dibelval3  36928  dib1dim  36946  dvh2dim  37226  mapd0  37446  hdmap14lem13  37661  pellexlem5  37899  jm2.23  38064  flcidc  38245  snhesn  38580  snssiALTVD  39556  snssiALT  39557  fsneq  39885  iccintsng  40230  icoiccdif  40231  limcrecl  40341  lptioo2  40343  lptioo1  40344  limcresiooub  40354  limcresioolb  40355  cnrefiisplem  40535  icccncfext  40580  dvmptfprodlem  40639  dvnprodlem3  40643  dirkercncflem2  40800  fourierdlem40  40843  fourierdlem48  40850  fourierdlem51  40853  fourierdlem62  40864  fourierdlem66  40868  fourierdlem74  40876  fourierdlem75  40877  fourierdlem76  40878  fourierdlem78  40880  fourierdlem79  40881  fourierdlem93  40895  fourierdlem101  40903  fourierdlem103  40905  fourierdlem104  40906  fouriersw  40927  elaa2  40930  etransclem44  40974  rrxsnicc  40999  sge00  41072  absnsb  41651  funressnfv  41662  dfdfat2  41717  tz6.12-afv  41762  tz6.12-afv2  41829  otiunsndisjX  41869  iccpartgtl  41937  iccpartgt  41938  iccpartleu  41939  iccpartgel  41940  nnsum4primeseven  42263  nnsum4primesevenALTV  42264  bgoldbtbnd  42272  xpsnopab  42333  opeliun2xp  42679  aacllem  43118