Theorem velsn 4589

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2111  {csn 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-sn 4574

This theorem is referenced by:  rabsneq  4592  dfpr2  4594  ralsnsg  4620  rexsns  4621  ralsng  4625  disjsn  4661  snprc  4667  snssb  4732  raldifsnb  4745  difprsnss  4748  pwpw0  4762  eqsn  4778  eqsndOLD  4780  snsspw  4793  dfnfc2  4878  uni0b  4882  uni0c  4883  iunid  5007  iunsn  5012  sndisj  5081  rext  5387  moabex  5397  exss  5401  otiunsndisj  5458  dffr6  5570  fconstmpt  5676  opeliunxp  5681  opeliun2xp  5682  rnep  5866  restidsing  6001  xpdifid  6115  dmsnopg  6160  sniota  6472  dfmpt3  6615  tz6.12-2  6809  nfunsn  6861  fnsnfv  6901  dffv2  6917  fsn  7068  fnasrn  7078  fnsnbg  7098  fnsnbOLD  7100  fmptsng  7102  fmptsnd  7103  fvclss  7175  eqfunresadj  7294  eusvobj2  7338  resf1extb  7864  opabex3d  7897  opabex3rd  7898  opabex3  7899  xpord2pred  8075  xpord3pred  8082  frrlem12  8227  frrlem13  8228  oarec  8477  mapdm0  8766  ixp0x  8850  snmapen  8960  xpsnen  8974  marypha2lem2  9320  elirrvOLD  9484  cantnfp1lem1  9568  cantnfp1lem3  9570  djuunxp  9814  dfac5lem1  10014  dfac5lem2  10015  dfac5lem4  10017  dfac5lem4OLD  10019  fin1a2lem11  10301  axdc4lem  10346  axcclem  10348  ttukeylem7  10406  xrsupexmnf  13204  xrinfmexpnf  13205  iccid  13290  fzsn  13466  fzpr  13479  seqz  13957  hashf1  14364  pr2pwpr  14386  s3iunsndisj  14875  fsum2dlem  15677  incexc2  15745  prodsn  15869  prodsnf  15871  fprod2dlem  15887  ef0lem  15985  lcmfunsnlem2  16551  1nprm  16590  vdwapun  16886  prmodvdslcmf  16959  cshwsiun  17011  chnccat  18532  mgmidsssn0  18580  mnd1id  18688  0subm  18725  efmnd1bas  18801  smndex1basss  18813  smndex1mgm  18815  trivsubgsnd  19066  kerf1ghm  19159  ghmqusnsglem1  19192  ghmquskerlem1  19195  ghmqusker  19199  symg1bas  19303  pmtrprfvalrn  19400  gex1  19503  sylow2alem1  19529  lsmdisj2  19594  0frgp  19691  0cyg  19805  prmcyg  19806  dprddisj2  19953  ablfacrp  19980  lspdisj  21062  lidlnz  21179  mulgrhm2  21415  pzriprnglem10  21427  ocvin  21611  psrlidm  21899  mplcoe1  21972  mplcoe5  21975  psdmul  22081  maducoeval2  22555  madugsum  22558  en2top  22900  restsn  23085  ist1-3  23264  ordtt1  23294  cmpcld  23317  unisngl  23442  dissnlocfin  23444  ptopn2  23499  snfil  23779  alexsubALTlem2  23963  alexsubALTlem3  23964  alexsubALTlem4  23965  haustsms2  24052  tsmsxplem1  24068  tsmsxplem2  24069  ust0  24135  dscopn  24488  nmoid  24657  limcdif  25804  ellimc2  25805  limcmpt  25811  limcres  25814  ply1remlem  26097  plyeq0lem  26142  plyremlem  26239  aaliou2  26275  radcnv0  26352  abelthlem2  26369  wilthlem2  27006  vmappw  27053  ppinprm  27089  chtnprm  27091  musumsum  27129  dchrhash  27209  lgsquadlem1  27318  lgsquadlem2  27319  eqscut3  27765  ssltleft  27815  ssltright  27816  cofcutr  27868  addsuniflem  27944  negsid  27983  negsunif  27997  ssltmul1  28086  ssltmul2  28087  precsexlem11  28155  onscutlt  28201  n0sfincut  28282  0reno  28399  cplgr1v  29408  rusgrnumwwlkb0  29952  frgrncvvdeq  30289  fusgr2wsp2nb  30314  hsn0elch  31228  cycpmrn  33112  qsxpid  33327  prmidl0  33415  ccfldextdgrr  33685  xrge0iifiso  33948  qqhval2  33995  esumnul  34061  esumrnmpt2  34081  esumfzf  34082  sibfof  34353  sitgaddlemb  34361  plymulx0  34560  signstf0  34581  prodfzo03  34616  circlemeth  34653  sconnpi1  35283  dffr5  35798  elima4  35820  brsingle  35959  dfiota3  35965  funpartfun  35987  dfrdg4  35995  fwddifn0  36208  bj-csbsnlem  36947  bj-axsn  37076  bj-axadj  37085  bj-pw0ALT  37093  bj-restsn  37126  bj-rest10  37132  mptsnunlem  37382  fvineqsneu  37455  matunitlindflem1  37655  poimirlem23  37682  poimirlem26  37685  poimirlem27  37686  grposnOLD  37921  0idl  38064  smprngopr  38091  isdmn3  38113  dfsucmap3  38475  ressn2  38543  lshpdisj  39085  lsat0cv  39131  snatpsubN  39848  dibelval3  41245  dib1dim  41263  dvh2dim  41543  mapd0  41763  hdmap14lem13  41978  dvrelogpow2b  42160  sticksstones11  42248  unitscyglem4  42290  sn-iotalem  42313  prjspeclsp  42704  pellexlem5  42925  jm2.23  43088  flcidc  43262  tfsconcatrn  43434  snhesn  43878  snssiALTVD  44918  snssiALT  44919  permaxinf2lem  45104  fsneq  45302  iccintsng  45622  icoiccdif  45623  limcrecl  45728  lptioo2  45730  lptioo1  45731  limcresiooub  45739  limcresioolb  45740  cnrefiisplem  45926  icccncfext  45984  dvmptfprodlem  46041  dvnprodlem3  46045  dirkercncflem2  46201  fourierdlem40  46244  fourierdlem48  46251  fourierdlem51  46254  fourierdlem62  46265  fourierdlem66  46269  fourierdlem74  46277  fourierdlem75  46278  fourierdlem76  46279  fourierdlem78  46281  fourierdlem79  46282  fourierdlem93  46296  fourierdlem101  46304  fourierdlem103  46306  fourierdlem104  46307  fouriersw  46328  elaa2  46331  etransclem44  46375  rrxsnicc  46397  sge00  46473  chnsubseq  46977  absnsb  47126  funressnfv  47142  fsetsniunop  47148  dfdfat2  47227  tz6.12-afv  47272  tz6.12-afv2  47339  otiunsndisjX  47378  iccpartgtl  47525  iccpartgt  47526  iccpartleu  47527  iccpartgel  47528  nnsum4primeseven  47899  nnsum4primesevenALTV  47900  bgoldbtbnd  47908  dfclnbgr6  47955  dfnbgr6  47956  stgredgiun  48057  xpsnopab  48256  mo0sn  48915  tposres0  48976  setcsnterm  49590  2arwcatlem1  49695  2arwcat  49700  setc1onsubc  49702  aacllem  49901