Theorem velsn 4644

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

Syntax hints:   ↔ wb 205   = wceq 1542   ∈ wcel 2107  {csn 4628

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-sn 4629

This theorem is referenced by:  dfpr2  4647  ralsnsg  4672  rexsns  4673  ralsng  4677  disjsn  4715  snprc  4721  snssb  4786  snssgOLD  4788  raldifsnb  4799  difprsnss  4802  pwpw0  4816  eqsn  4832  snsspw  4845  pwsnOLD  4901  dfnfc2  4933  uni0b  4937  uni0c  4938  iunid  5063  iunsn  5069  sndisj  5139  rext  5448  moabex  5459  exss  5463  otiunsndisj  5520  dffr6  5634  fconstmpt  5737  opeliunxp  5742  rnep  5925  restidsing  6051  xpdifid  6165  dmsnopg  6210  sniota  6532  dfmpt3  6682  nfunsn  6931  fnsnfv  6968  dffv2  6984  fsn  7130  fnasrn  7140  fnsnb  7161  fmptsng  7163  fmptsnd  7164  fvclss  7238  eqfunresadj  7354  eusvobj2  7398  sucexeloniOLD  7795  suceloniOLD  7797  opabex3d  7949  opabex3rd  7950  opabex3  7951  xpord2pred  8128  xpord3pred  8135  frrlem12  8279  frrlem13  8280  wfrlem14OLD  8319  wfrlem15OLD  8320  oarec  8559  mapdm0  8833  ixp0x  8917  snmapen  9035  xpsnen  9052  marypha2lem2  9428  elirrv  9588  cantnfp1lem1  9670  cantnfp1lem3  9672  djuunxp  9913  dfac5lem1  10115  dfac5lem2  10116  dfac5lem4  10118  fin1a2lem11  10402  axdc4lem  10447  axcclem  10449  ttukeylem7  10507  xrsupexmnf  13281  xrinfmexpnf  13282  iccid  13366  fzsn  13540  fzpr  13553  seqz  14013  hashf1  14415  pr2pwpr  14437  s3iunsndisj  14912  fsum2dlem  15713  incexc2  15781  prodsn  15903  prodsnf  15905  fprod2dlem  15921  ef0lem  16019  lcmfunsnlem2  16574  1nprm  16613  vdwapun  16904  prmodvdslcmf  16977  cshwsiun  17030  mgmidsssn0  18588  mnd1id  18665  0subm  18695  efmnd1bas  18771  smndex1basss  18783  smndex1mgm  18785  trivsubgsnd  19029  symg1bas  19253  pmtrprfvalrn  19351  gex1  19454  sylow2alem1  19480  lsmdisj2  19545  0frgp  19642  0cyg  19756  prmcyg  19757  dprddisj2  19904  ablfacrp  19931  kerf1ghm  20275  lspdisj  20731  lidlnz  20846  mulgrhm2  21040  ocvin  21219  psrlidm  21515  mplcoe1  21584  mplcoe5  21587  maducoeval2  22134  madugsum  22137  en2top  22480  restsn  22666  ist1-3  22845  ordtt1  22875  cmpcld  22898  unisngl  23023  dissnlocfin  23025  ptopn2  23080  snfil  23360  alexsubALTlem2  23544  alexsubALTlem3  23545  alexsubALTlem4  23546  haustsms2  23633  tsmsxplem1  23649  tsmsxplem2  23650  ust0  23716  dscopn  24074  nmoid  24251  limcdif  25385  ellimc2  25386  limcmpt  25392  limcres  25395  ply1remlem  25672  plyeq0lem  25716  plyremlem  25809  aaliou2  25845  radcnv0  25920  abelthlem2  25936  wilthlem2  26563  vmappw  26610  ppinprm  26646  chtnprm  26648  musumsum  26686  dchrhash  26764  lgsquadlem1  26873  lgsquadlem2  26874  ssltleft  27355  ssltright  27356  cofcutr  27401  addsuniflem  27474  negsid  27505  negsunif  27519  ssltmul1  27592  ssltmul2  27593  precsexlem11  27653  cplgr1v  28677  rusgrnumwwlkb0  29215  frgrncvvdeq  29552  fusgr2wsp2nb  29577  hsn0elch  30489  eqsnd  31754  cycpmrn  32290  qsxpid  32463  ghmquskerlem1  32517  ghmqusker  32521  prmidl0  32558  ccfldextdgrr  32735  xrge0iifiso  32904  qqhval2  32951  esumnul  33035  esumrnmpt2  33055  esumfzf  33056  sibfof  33328  sitgaddlemb  33336  plymulx0  33547  signstf0  33568  prodfzo03  33604  circlemeth  33641  sconnpi1  34219  dffr5  34713  elima4  34736  brsingle  34878  dfiota3  34884  funpartfun  34904  dfrdg4  34912  fwddifn0  35125  bj-csbsnlem  35772  bj-axsn  35902  bj-axadj  35911  bj-pw0ALT  35919  bj-restsn  35952  bj-rest10  35958  mptsnunlem  36208  fvineqsneu  36281  matunitlindflem1  36473  poimirlem23  36500  poimirlem26  36503  poimirlem27  36504  grposnOLD  36739  0idl  36882  smprngopr  36909  isdmn3  36931  ressn2  37301  lshpdisj  37846  lsat0cv  37892  snatpsubN  38610  dibelval3  40007  dib1dim  40025  dvh2dim  40305  mapd0  40525  hdmap14lem13  40740  dvrelogpow2b  40922  sticksstones11  40961  sn-iotalem  41035  fnsnbt  41049  prjspeclsp  41351  pellexlem5  41557  jm2.23  41721  flcidc  41902  tfsconcatrn  42078  snhesn  42523  snssiALTVD  43574  snssiALT  43575  fsneq  43891  iccintsng  44223  icoiccdif  44224  limcrecl  44332  lptioo2  44334  lptioo1  44335  limcresiooub  44345  limcresioolb  44346  cnrefiisplem  44532  icccncfext  44590  dvmptfprodlem  44647  dvnprodlem3  44651  dirkercncflem2  44807  fourierdlem40  44850  fourierdlem48  44857  fourierdlem51  44860  fourierdlem62  44871  fourierdlem66  44875  fourierdlem74  44883  fourierdlem75  44884  fourierdlem76  44885  fourierdlem78  44887  fourierdlem79  44888  fourierdlem93  44902  fourierdlem101  44910  fourierdlem103  44912  fourierdlem104  44913  fouriersw  44934  elaa2  44937  etransclem44  44981  rrxsnicc  45003  sge00  45079  absnsb  45724  funressnfv  45740  fsetsniunop  45746  dfdfat2  45823  tz6.12-afv  45868  tz6.12-afv2  45935  otiunsndisjX  45974  iccpartgtl  46081  iccpartgt  46082  iccpartleu  46083  iccpartgel  46084  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  bgoldbtbnd  46464  xpsnopab  46522  opeliun2xp  46962  mo0sn  47454  aacllem  47802