Theorem velsn 4574

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

Syntax hints:   ↔ wb 208   = wceq 1548   ∈ wcel 2121  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-sn 4559

This theorem is referenced by:  rabsneq  4577  dfpr2  4579  ralsnsg  4605  rexsns  4606  ralsng  4610  disjsn  4646  snprc  4652  snssb  4717  raldifsnb  4732  difprsnss  4735  pwpw0  4747  eqsn  4763  eqsndOLD  4765  snsspw  4778  dfnfc2  4863  uni0b  4867  uni0c  4868  iunid  4993  iunsn  4998  rext  5390  moabexOLD  5401  exss  5405  otiunsndisj  5464  dffr6  5577  fconstmpt  5683  opeliunxp  5688  opeliun2xp  5689  rnep  5876  restidsing  6012  xpdifid  6123  dmsnopg  6168  sniota  6480  dfmpt3  6623  tz6.12-2  6818  nfunsn  6870  fnsnfv  6910  dffv2  6926  fsneq  6980  fsn  7081  fnasrn  7091  fnsnbg  7112  fnsnbOLD  7114  fmptsng  7116  fmptsnd  7117  fvclss  7189  eqfunresadj  7308  eusvobj2  7352  resf1extb  7878  opabex3d  7911  opabex3rd  7912  opabex3  7913  xpord2pred  8089  xpord3pred  8096  frrlem12  8241  frrlem13  8242  oarec  8491  mapdm0  8783  ixp0x  8868  snmapen  8979  xpsnen  8993  marypha2lem2  9343  elirrvOLDOLD  9508  cantnfp1lem1  9594  cantnfp1lem3  9596  djuunxp  9840  dfac5lem1  10040  dfac5lem2  10041  dfac5lem4  10043  dfac5lem4OLD  10045  fin1a2lem11  10327  axdc4lem  10372  axcclem  10374  ttukeylem7  10432  xrsupexmnf  13252  xrinfmexpnf  13253  iccid  13338  fzsn  13515  fzpr  13528  seqz  14007  hashf1  14414  pr2pwpr  14436  s3iunsndisj  14925  fsum2dlem  15727  incexc2  15798  prodsn  15922  prodsnf  15924  fprod2dlem  15940  ef0lem  16038  lcmfunsnlem2  16604  1nprm  16643  vdwapun  16940  prmodvdslcmf  17013  cshwsiun  17065  chnccat  18587  mgmidsssn0  18635  mnd1id  18743  0subm  18780  efmnd1bas  18856  smndex1basss  18871  smndex1mgm  18873  trivsubgsnd  19124  kerf1ghm  19217  ghmqusnsglem1  19250  ghmquskerlem1  19253  ghmqusker  19257  symg1bas  19361  pmtrprfvalrn  19458  gex1  19561  sylow2alem1  19587  lsmdisj2  19652  0frgp  19749  0cyg  19863  prmcyg  19864  dprddisj2  20011  ablfacrp  20038  lspdisj  21122  lidlnz  21239  mulgrhm2  21457  pzriprnglem10  21469  ocvin  21653  psrlidm  21940  mplcoe1  22017  mplcoe5  22020  psdmul  22158  maducoeval2  22627  madugsum  22630  en2top  22972  restsn  23157  ist1-3  23336  ordtt1  23366  cmpcld  23389  unisngl  23514  dissnlocfin  23516  ptopn2  23571  snfil  23851  alexsubALTlem2  24035  alexsubALTlem3  24036  alexsubALTlem4  24037  haustsms2  24124  tsmsxplem1  24140  tsmsxplem2  24141  ust0  24207  dscopn  24560  nmoid  24729  limcdif  25865  ellimc2  25866  limcmpt  25872  limcres  25875  ply1remlem  26152  plyeq0lem  26197  plyremlem  26292  aaliou2  26328  radcnv0  26403  abelthlem2  26419  wilthlem2  27054  vmappw  27101  ppinprm  27137  chtnprm  27139  musumsum  27177  dchrhash  27256  lgsquadlem1  27365  lgsquadlem2  27366  eqcuts3  27818  sltsleft  27874  sltsright  27875  cofcutr  27938  addsuniflem  28015  negsid  28055  negsunif  28069  sltmuls1  28161  sltmuls2  28162  precsexlem11  28231  oncutlt  28278  n0fincut  28369  elreno2  28509  cplgr1v  29521  rusgrnumwwlkb0  30064  frgrncvvdeq  30401  fusgr2wsp2nb  30426  hsn0elch  31341  indsn  32946  cycpmrn  33228  qsxpid  33449  prmidl0  33537  mvrvalind  33734  mplmonprod  33750  esplyfvaln  33770  esplyind  33771  ccfldextdgrr  33868  xrge0iifiso  34131  qqhval2  34178  esumnul  34244  esumrnmpt2  34264  esumfzf  34265  sibfof  34536  sitgaddlemb  34544  plymulx0  34743  signstf0  34764  prodfzo03  34799  circlemeth  34836  sconnpi1  35482  dffr5  35997  elima4  36019  brsingle  36158  dfiota3  36164  funpartfun  36186  dfrdg4  36194  fwddifn0  36407  mh-infprim2bi  36790  mh-infprim3bi  36791  bj-csbsnlem  37271  bj-axsn  37400  bj-axadj  37409  bj-pw0ALT  37417  bj-restsn  37455  bj-rest10  37461  mptsnunlem  37715  fvineqsneu  37788  matunitlindflem1  37998  poimirlem23  38025  poimirlem26  38028  poimirlem27  38029  grposnOLD  38264  0idl  38407  smprngopr  38434  isdmn3  38456  dfsucmap3  38845  ressn2  38914  lshpdisj  39494  lsat0cv  39540  snatpsubN  40257  dibelval3  41654  dib1dim  41672  dvh2dim  41952  mapd0  42172  hdmap14lem13  42387  dvrelogpow2b  42568  sticksstones11  42656  unitscyglem4  42698  sn-iotalem  42723  prjspeclsp  43077  pellexlem5  43293  jm2.23  43456  flcidc  43630  tfsconcatrn  43802  snhesn  44245  snssiALTVD  45285  snssiALT  45286  permaxinf2lem  45471  iccintsng  45982  icoiccdif  45983  limcrecl  46088  lptioo2  46090  lptioo1  46091  limcresiooub  46099  limcresioolb  46100  cnrefiisplem  46286  icccncfext  46344  dvmptfprodlem  46401  dvnprodlem3  46405  dirkercncflem2  46561  fourierdlem40  46604  fourierdlem48  46611  fourierdlem51  46614  fourierdlem62  46625  fourierdlem66  46629  fourierdlem74  46637  fourierdlem75  46638  fourierdlem76  46639  fourierdlem78  46641  fourierdlem79  46642  fourierdlem93  46656  fourierdlem101  46664  fourierdlem103  46666  fourierdlem104  46667  fouriersw  46688  elaa2  46691  etransclem44  46735  rrxsnicc  46757  sge00  46833  chnsubseq  47339  absnsb  47504  funressnfv  47520  fsetsniunop  47526  dfdfat2  47605  tz6.12-afv  47650  tz6.12-afv2  47717  otiunsndisjX  47756  iccpartgtl  47915  iccpartgt  47916  iccpartleu  47917  iccpartgel  47918  nnsum4primeseven  48305  nnsum4primesevenALTV  48306  bgoldbtbnd  48314  dfclnbgr6  48361  dfnbgr6  48362  stgredgiun  48463  xpsnopab  48662  mo0sn  49320  tposres0  49381  setcsnterm  49994  2arwcatlem1  50099  2arwcat  50104  setc1onsubc  50106  aacllem  50305