Theorem velsn 4584

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {csn 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-sn 4569

This theorem is referenced by:  rabsneq  4587  dfpr2  4589  ralsnsg  4615  rexsns  4616  ralsng  4620  disjsn  4656  snprc  4662  snssb  4727  raldifsnb  4740  difprsnss  4743  pwpw0  4757  eqsn  4773  eqsndOLD  4775  snsspw  4788  dfnfc2  4873  uni0b  4877  uni0c  4878  iunid  5004  iunsn  5009  rext  5397  moabexOLD  5408  exss  5412  otiunsndisj  5470  dffr6  5582  fconstmpt  5688  opeliunxp  5693  opeliun2xp  5694  rnep  5878  restidsing  6014  xpdifid  6128  dmsnopg  6173  sniota  6485  dfmpt3  6628  tz6.12-2  6823  nfunsn  6875  fnsnfv  6915  dffv2  6931  fsn  7084  fnasrn  7094  fnsnbg  7114  fnsnbOLD  7116  fmptsng  7118  fmptsnd  7119  fvclss  7191  eqfunresadj  7310  eusvobj2  7354  resf1extb  7880  opabex3d  7913  opabex3rd  7914  opabex3  7915  xpord2pred  8090  xpord3pred  8097  frrlem12  8242  frrlem13  8243  oarec  8492  mapdm0  8784  ixp0x  8869  snmapen  8980  xpsnen  8994  marypha2lem2  9344  elirrvOLD  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  21119  lidlnz  21236  mulgrhm2  21472  pzriprnglem10  21484  ocvin  21668  psrlidm  21954  mplcoe1  22029  mplcoe5  22032  psdmul  22146  maducoeval2  22619  madugsum  22622  en2top  22964  restsn  23149  ist1-3  23328  ordtt1  23358  cmpcld  23381  unisngl  23506  dissnlocfin  23508  ptopn2  23563  snfil  23843  alexsubALTlem2  24027  alexsubALTlem3  24028  alexsubALTlem4  24029  haustsms2  24116  tsmsxplem1  24132  tsmsxplem2  24133  ust0  24199  dscopn  24552  nmoid  24721  limcdif  25857  ellimc2  25858  limcmpt  25864  limcres  25867  ply1remlem  26144  plyeq0lem  26189  plyremlem  26285  aaliou2  26321  radcnv0  26398  abelthlem2  26414  wilthlem2  27050  vmappw  27097  ppinprm  27133  chtnprm  27135  musumsum  27173  dchrhash  27252  lgsquadlem1  27361  lgsquadlem2  27362  eqcuts3  27814  sltsleft  27870  sltsright  27871  cofcutr  27934  addsuniflem  28011  negsid  28051  negsunif  28065  sltmuls1  28157  sltmuls2  28158  precsexlem11  28227  oncutlt  28274  n0fincut  28365  elreno2  28505  cplgr1v  29517  rusgrnumwwlkb0  30061  frgrncvvdeq  30398  fusgr2wsp2nb  30423  hsn0elch  31338  indsn  32942  cycpmrn  33223  qsxpid  33441  prmidl0  33529  mvrvalind  33701  mplmonprod  33717  esplyfvaln  33737  esplyind  33738  ccfldextdgrr  33836  xrge0iifiso  34099  qqhval2  34146  esumnul  34212  esumrnmpt2  34232  esumfzf  34233  sibfof  34504  sitgaddlemb  34512  plymulx0  34711  signstf0  34732  prodfzo03  34767  circlemeth  34804  sconnpi1  35441  dffr5  35956  elima4  35978  brsingle  36117  dfiota3  36123  funpartfun  36145  dfrdg4  36153  fwddifn0  36366  mh-infprim2bi  36749  mh-infprim3bi  36750  bj-csbsnlem  37230  bj-axsn  37359  bj-axadj  37368  bj-pw0ALT  37376  bj-restsn  37414  bj-rest10  37420  mptsnunlem  37672  fvineqsneu  37745  matunitlindflem1  37955  poimirlem23  37982  poimirlem26  37985  poimirlem27  37986  grposnOLD  38221  0idl  38364  smprngopr  38391  isdmn3  38413  dfsucmap3  38802  ressn2  38871  lshpdisj  39451  lsat0cv  39497  snatpsubN  40214  dibelval3  41611  dib1dim  41629  dvh2dim  41909  mapd0  42129  hdmap14lem13  42344  dvrelogpow2b  42525  sticksstones11  42613  unitscyglem4  42655  sn-iotalem  42680  prjspeclsp  43063  pellexlem5  43283  jm2.23  43446  flcidc  43620  tfsconcatrn  43792  snhesn  44235  snssiALTVD  45275  snssiALT  45276  permaxinf2lem  45461  fsneq  45657  iccintsng  45975  icoiccdif  45976  limcrecl  46081  lptioo2  46083  lptioo1  46084  limcresiooub  46092  limcresioolb  46093  cnrefiisplem  46279  icccncfext  46337  dvmptfprodlem  46394  dvnprodlem3  46398  dirkercncflem2  46554  fourierdlem40  46597  fourierdlem48  46604  fourierdlem51  46607  fourierdlem62  46618  fourierdlem66  46622  fourierdlem74  46630  fourierdlem75  46631  fourierdlem76  46632  fourierdlem78  46634  fourierdlem79  46635  fourierdlem93  46649  fourierdlem101  46657  fourierdlem103  46659  fourierdlem104  46660  fouriersw  46681  elaa2  46684  etransclem44  46728  rrxsnicc  46750  sge00  46826  chnsubseq  47330  absnsb  47491  funressnfv  47507  fsetsniunop  47513  dfdfat2  47592  tz6.12-afv  47637  tz6.12-afv2  47704  otiunsndisjX  47743  iccpartgtl  47902  iccpartgt  47903  iccpartleu  47904  iccpartgel  47905  nnsum4primeseven  48292  nnsum4primesevenALTV  48293  bgoldbtbnd  48301  dfclnbgr6  48348  dfnbgr6  48349  stgredgiun  48450  xpsnopab  48649  mo0sn  49307  tposres0  49368  setcsnterm  49981  2arwcatlem1  50086  2arwcat  50091  setc1onsubc  50093  aacllem  50292