Theorem velsn 4577

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

Syntax hints:   ↔ wb 205   = wceq 1539   ∈ wcel 2106  {csn 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-sn 4562

This theorem is referenced by:  dfpr2  4580  ralsnsg  4604  rexsns  4605  ralsng  4609  disjsn  4647  snprc  4653  snssg  4718  raldifsnb  4729  difprsnss  4732  pwpw0  4746  eqsn  4762  snsspw  4775  pwsnOLD  4832  dfnfc2  4863  uni0b  4867  uni0c  4868  iunsn  4995  sndisj  5065  rext  5364  moabex  5374  exss  5378  otiunsndisj  5434  dffr6  5547  fconstmpt  5649  opeliunxp  5654  rnep  5836  restidsing  5962  xpdifid  6071  dmsnopg  6116  sniota  6424  dfmpt3  6567  nfunsn  6811  fnsnfv  6847  dffv2  6863  fsn  7007  fnasrn  7017  fnsnb  7038  fmptsng  7040  fmptsnd  7041  fvclss  7115  eusvobj2  7268  sucexeloni  7658  suceloniOLD  7660  opabex3d  7808  opabex3rd  7809  opabex3  7810  frrlem12  8113  frrlem13  8114  wfrlem14OLD  8153  wfrlem15OLD  8154  oarec  8393  mapdm0  8630  ixp0x  8714  snmapen  8828  xpsnen  8842  marypha2lem2  9195  elirrv  9355  cantnfp1lem1  9436  cantnfp1lem3  9438  djuunxp  9679  dfac5lem1  9879  dfac5lem2  9880  dfac5lem4  9882  fin1a2lem11  10166  axdc4lem  10211  axcclem  10213  ttukeylem7  10271  xrsupexmnf  13039  xrinfmexpnf  13040  iccid  13124  fzsn  13298  fzpr  13311  seqz  13771  hashf1  14171  pr2pwpr  14193  s3iunsndisj  14679  fsum2dlem  15482  incexc2  15550  prodsn  15672  prodsnf  15674  fprod2dlem  15690  ef0lem  15788  lcmfunsnlem2  16345  1nprm  16384  vdwapun  16675  prmodvdslcmf  16748  cshwsiun  16801  mgmidsssn0  18356  mnd1id  18427  0subm  18456  efmnd1bas  18532  smndex1basss  18544  smndex1mgm  18546  trivsubgsnd  18782  symg1bas  18998  pmtrprfvalrn  19096  gex1  19196  sylow2alem1  19222  lsmdisj2  19288  0frgp  19385  0cyg  19494  prmcyg  19495  dprddisj2  19642  ablfacrp  19669  kerf1ghm  19987  lspdisj  20387  lidlnz  20499  mulgrhm2  20700  ocvin  20879  psrlidm  21172  mplcoe1  21238  mplcoe5  21241  maducoeval2  21789  madugsum  21792  en2top  22135  restsn  22321  ist1-3  22500  ordtt1  22530  cmpcld  22553  unisngl  22678  dissnlocfin  22680  ptopn2  22735  snfil  23015  alexsubALTlem2  23199  alexsubALTlem3  23200  alexsubALTlem4  23201  haustsms2  23288  tsmsxplem1  23304  tsmsxplem2  23305  ust0  23371  dscopn  23729  nmoid  23906  limcdif  25040  ellimc2  25041  limcmpt  25047  limcres  25050  ply1remlem  25327  plyeq0lem  25371  plyremlem  25464  aaliou2  25500  radcnv0  25575  abelthlem2  25591  wilthlem2  26218  vmappw  26265  ppinprm  26301  chtnprm  26303  musumsum  26341  dchrhash  26419  lgsquadlem1  26528  lgsquadlem2  26529  cplgr1v  27797  rusgrnumwwlkb0  28336  frgrncvvdeq  28673  fusgr2wsp2nb  28698  hsn0elch  29610  eqsnd  30877  cycpmrn  31410  qsxpid  31558  prmidl0  31626  ccfldextdgrr  31742  xrge0iifiso  31885  qqhval2  31932  esumnul  32016  esumrnmpt2  32036  esumfzf  32037  sibfof  32307  sitgaddlemb  32315  plymulx0  32526  signstf0  32547  prodfzo03  32583  circlemeth  32620  bnj521  32716  sconnpi1  33201  dffr5  33721  eqfunresadj  33735  elima4  33750  xpord2pred  33792  xpord3pred  33798  ssltleft  34054  ssltright  34055  cofcutr  34092  brsingle  34219  dfiota3  34225  funpartfun  34245  dfrdg4  34253  fwddifn0  34466  bj-csbsnlem  35088  bj-pw0ALT  35222  bj-restsn  35253  bj-rest10  35259  mptsnunlem  35509  fvineqsneu  35582  matunitlindflem1  35773  poimirlem23  35800  poimirlem26  35803  poimirlem27  35804  grposnOLD  36040  0idl  36183  smprngopr  36210  isdmn3  36232  lshpdisj  37001  lsat0cv  37047  snatpsubN  37764  dibelval3  39161  dib1dim  39179  dvh2dim  39459  mapd0  39679  hdmap14lem13  39894  dvrelogpow2b  40076  sticksstones11  40112  sn-iotalem  40189  fnsnbt  40208  prjspeclsp  40451  prjcrv0  40470  pellexlem5  40655  jm2.23  40818  flcidc  40999  snhesn  41394  snssiALTVD  42447  snssiALT  42448  fsneq  42746  iccintsng  43061  icoiccdif  43062  limcrecl  43170  lptioo2  43172  lptioo1  43173  limcresiooub  43183  limcresioolb  43184  cnrefiisplem  43370  icccncfext  43428  dvmptfprodlem  43485  dvnprodlem3  43489  dirkercncflem2  43645  fourierdlem40  43688  fourierdlem48  43695  fourierdlem51  43698  fourierdlem62  43709  fourierdlem66  43713  fourierdlem74  43721  fourierdlem75  43722  fourierdlem76  43723  fourierdlem78  43725  fourierdlem79  43726  fourierdlem93  43740  fourierdlem101  43748  fourierdlem103  43750  fourierdlem104  43751  fouriersw  43772  elaa2  43775  etransclem44  43819  rrxsnicc  43841  sge00  43914  absnsb  44521  funressnfv  44537  fsetsniunop  44543  dfdfat2  44620  tz6.12-afv  44665  tz6.12-afv2  44732  otiunsndisjX  44771  iccpartgtl  44878  iccpartgt  44879  iccpartleu  44880  iccpartgel  44881  nnsum4primeseven  45252  nnsum4primesevenALTV  45253  bgoldbtbnd  45261  xpsnopab  45319  opeliun2xp  45668  mo0sn  46161  aacllem  46505