Theorem velsn 4607

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2146  {csn 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-sn 4592

This theorem is used by:  rabsneq  4610  dfpr2  4612  ralsnsg  4638  rexsns  4639  ralsng  4643  disjsn  4679  snprc  4685  snssb  4750  raldifsnb  4766  difprsnss  4769  pwpw0  4781  eqsn  4797  snsspw  4811  dfnfc2  4896  uni0b  4901  uni0c  4902  iunid  5027  iunsn  5032  rext  5431  moabexOLD  5442  exss  5446  otiunsndisj  5505  dffr6  5619  fconstmpt  5725  opeliunxp  5730  opeliun2xp  5731  rnep  5919  restidsing  6057  xpdifid  6168  dmsnopg  6217  sniota  6532  dfmpt3  6674  tz6.12-2  6873  nfunsn  6925  fnsnfv  6965  dffv2  6981  fsneq  7035  fsn  7136  fnasrn  7148  fnsnbg  7169  fnsnbOLD  7171  fmptsng  7173  fmptsnd  7174  fvclss  7245  eqfunresadj  7370  eusvobj2  7412  resf1extb  7938  opabex3d  7969  opabex3rd  7970  opabex3  7971  xpord2pred  8148  xpord3pred  8155  frrlem12  8301  frrlem13  8302  oarec  8554  mapdm0  8846  ixp0x  8931  snmapen  9043  xpsnen  9057  marypha2lem2  9404  elirrvOLDOLD  9569  cantnfp1lem1  9655  cantnfp1lem3  9657  djuunxp  9924  dfac5lem1  10124  dfac5lem2  10125  dfac5lem4  10127  fin1a2lem11  10410  axdc4lem  10455  axcclem  10457  ttukeylem7  10515  xrsupexmnf  13352  xrinfmexpnf  13353  iccid  13438  fzsn  13616  fzpr  13629  seqz  14109  hashf1  14517  pr2pwpr  14539  s3iunsndisj  15034  fsum2dlem  15849  incexc2  15920  prodsn  16044  prodsnf  16046  fprod2dlem  16062  ef0lem  16159  lcmfunsnlem2  16725  1nprm  16764  vdwapun  17061  prmodvdslcmf  17134  cshwsiun  17186  chnccat  18709  mgmidsssn0  18761  mnd1id  18880  0subm  18918  efmnd1bas  18994  smndex1basss  19009  smndex1mgm  19011  trivsubgsnd  19269  qsxpid  19292  kerf1ghm  19366  ghmqusnsglem1  19399  ghmquskerlem1  19402  ghmqusker  19406  symg1bas  19510  pmtrprfvalrn  19607  gex1  19710  sylow2alem1  19736  lsmdisj2  19801  0frgp  19898  0cyg  20012  prmcyg  20013  dprddisj2  20160  ablfacrp  20187  lspdisj  21304  lidlnz  21431  prmidl0  21533  mulgrhm2  21683  pzriprnglem10  21695  ocvin  21879  psrlidm  22166  mplcoe1  22243  mplcoe5  22246  psdmul  22384  maducoeval2  22852  madugsum  22855  en2top  23197  restsn  23382  ist1-3  23561  ordtt1  23591  cmpcld  23614  unisngl  23740  dissnlocfin  23742  ptopn2  23797  snfil  24077  alexsubALTlem2  24261  alexsubALTlem3  24262  alexsubALTlem4  24263  haustsms2  24350  tsmsxplem1  24366  tsmsxplem2  24367  ust0  24433  dscopn  24786  nmoid  24955  limcdif  26091  ellimc2  26092  limcmpt  26098  limcres  26101  ply1remlem  26378  plyeq0lem  26423  plyn0mulidp  26498  plyremlem  26521  aaliou2  26559  radcnv0  26635  abelthlem2  26651  wilthlem2  27289  vmappw  27336  ppinprm  27372  chtnprm  27374  musumsum  27412  dchrhash  27491  lgsquadlem1  27600  lgsquadlem2  27601  eqcuts3  28053  sltsleft  28109  sltsright  28110  cofcutr  28173  addsuniflem  28250  negsid  28290  negsunif  28304  sltmuls1  28396  sltmuls2  28397  precsexlem11  28466  oncutlt  28513  n0fincut  28604  elreno2  28744  cplgr1v  29843  rusgrnumwwlkb0  30395  frgrncvvdeq  30736  fusgr2wsp2nb  30761  hsn0elch  31676  indsn  33258  cycpmrn  33532  mvrvalind  33997  mplmonprod  34013  esplyfvaln  34033  esplyind  34034  ccfldextdgrr  34131  xrge0iifiso  34394  qqhval2  34441  esumnul  34507  esumrnmpt2  34527  esumfzf  34528  sibfof  34800  sitgaddlemb  34808  signstf0  35025  prodfzo03  35060  circlemeth  35097  scottsn  35582  kard0  35629  sconnpi1  35773  dffr5  36288  elima4  36310  brsingle  36449  dfiota3  36455  funpartfun  36477  dfrdg4  36485  fwddifn0  36698  mh-infprim2bi  37120  mh-infprim3bi  37121  bj-csbsnlem  37600  bj-axsn  37730  bj-axadj  37739  bj-pw0ALT  37747  bj-restsn  37786  bj-rest10  37792  mptsnunlem  38046  fvineqsneu  38119  matunitlindflem1  38329  poimirlem23  38356  poimirlem26  38359  poimirlem27  38360  grposnOLD  38596  0idl  38739  smprngopr  38766  isdmn3  38788  dfsucmap3  39175  ressn2  39244  lshpdisj  39824  lsat0cv  39870  snatpsubN  40587  dibelval3  41984  dib1dim  42002  dvh2dim  42282  mapd0  42502  hdmap14lem13  42717  dvrelogpow2b  42898  sticksstones11  42986  unitscyglem4  43028  sn-iotalem  43055  prjspeclsp  43422  pellexlem5  43638  jm2.23  43801  flcidc  43975  tfsconcatrn  44147  snhesn  44590  snssiALTVD  45613  snssiALT  45614  permaxinf2lem  45799  iccintsng  46317  icoiccdif  46318  limcrecl  46423  lptioo2  46425  lptioo1  46426  limcresiooub  46434  limcresioolb  46435  cnrefiisplem  46621  icccncfext  46679  dvmptfprodlem  46736  dvnprodlem3  46740  dirkercncflem2  46896  fourierdlem40  46939  fourierdlem48  46946  fourierdlem51  46949  fourierdlem62  46960  fourierdlem66  46964  fourierdlem74  46972  fourierdlem75  46973  fourierdlem76  46974  fourierdlem78  46976  fourierdlem79  46977  fourierdlem93  46991  fourierdlem101  46999  fourierdlem103  47001  fourierdlem104  47002  fouriersw  47023  elaa2  47026  etransclem44  47070  rrxsnicc  47092  sge00  47168  chnsubseq  47674  absnsb  47842  funressnfv  47858  fsetsniunop  47864  dfdfat2  47943  tz6.12-afv  47988  tz6.12-afv2  48055  otiunsndisjX  48094  iccpartgtl  48253  iccpartgt  48254  iccpartleu  48255  iccpartgel  48256  nnsum4primeseven  48643  nnsum4primesevenALTV  48644  bgoldbtbnd  48652  dfclnbgr6  48699  dfnbgr6  48700  stgredgiun  48801  xpsnopab  49000  smprngprmrng  49181  isidom3  49187  mo0sn  49671  tposres0  49732  setcsnterm  50345  2arwcatlem1  50450  2arwcat  50455  setc1onsubc  50457  aacllem  50698