Theorem velsn 4605

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-sn 4590

This theorem is used by:  rabsneq  4608  dfpr2  4610  ralsnsg  4636  rexsns  4637  ralsng  4641  disjsn  4677  snprc  4683  snssb  4748  raldifsnb  4764  difprsnss  4767  pwpw0  4779  eqsn  4795  snsspw  4809  dfnfc2  4894  uni0b  4899  uni0c  4900  iunid  5025  iunsn  5030  rext  5429  moabexOLD  5440  exss  5444  otiunsndisj  5503  dffr6  5617  fconstmpt  5723  opeliunxp  5728  opeliun2xp  5729  rnep  5917  restidsing  6055  xpdifid  6165  dmsnopg  6214  sniota  6527  dfmpt3  6669  tz6.12-2  6868  nfunsn  6920  fnsnfv  6960  dffv2  6976  fsneq  7030  fsn  7131  fnasrn  7141  fnsnbg  7162  fnsnbOLD  7164  fmptsng  7166  fmptsnd  7167  fvclss  7239  eqfunresadj  7358  eusvobj2  7402  resf1extb  7927  opabex3d  7958  opabex3rd  7959  opabex3  7960  xpord2pred  8137  xpord3pred  8144  frrlem12  8290  frrlem13  8291  oarec  8543  mapdm0  8835  ixp0x  8920  snmapen  9031  xpsnen  9045  marypha2lem2  9392  elirrvOLDOLD  9557  cantnfp1lem1  9643  cantnfp1lem3  9645  djuunxp  9912  dfac5lem1  10112  dfac5lem2  10113  dfac5lem4  10115  fin1a2lem11  10398  axdc4lem  10443  axcclem  10445  ttukeylem7  10503  xrsupexmnf  13335  xrinfmexpnf  13336  iccid  13421  fzsn  13599  fzpr  13612  seqz  14091  hashf1  14499  pr2pwpr  14521  s3iunsndisj  15010  fsum2dlem  15826  incexc2  15897  prodsn  16021  prodsnf  16023  fprod2dlem  16039  ef0lem  16136  lcmfunsnlem2  16702  1nprm  16741  vdwapun  17038  prmodvdslcmf  17111  cshwsiun  17163  chnccat  18686  mgmidsssn0  18734  mnd1id  18842  0subm  18880  efmnd1bas  18956  smndex1basss  18971  smndex1mgm  18973  trivsubgsnd  19224  qsxpid  19247  kerf1ghm  19321  ghmqusnsglem1  19354  ghmquskerlem1  19357  ghmqusker  19361  symg1bas  19465  pmtrprfvalrn  19562  gex1  19665  sylow2alem1  19691  lsmdisj2  19756  0frgp  19853  0cyg  19967  prmcyg  19968  dprddisj2  20115  ablfacrp  20142  lspdisj  21258  lidlnz  21385  prmidl0  21487  mulgrhm2  21637  pzriprnglem10  21649  ocvin  21833  psrlidm  22120  mplcoe1  22197  mplcoe5  22200  psdmul  22338  maducoeval2  22806  madugsum  22809  en2top  23151  restsn  23336  ist1-3  23515  ordtt1  23545  cmpcld  23568  unisngl  23693  dissnlocfin  23695  ptopn2  23750  snfil  24030  alexsubALTlem2  24214  alexsubALTlem3  24215  alexsubALTlem4  24216  haustsms2  24303  tsmsxplem1  24319  tsmsxplem2  24320  ust0  24386  dscopn  24739  nmoid  24908  limcdif  26044  ellimc2  26045  limcmpt  26051  limcres  26054  ply1remlem  26331  plyeq0lem  26376  plyn0mulidp  26451  plyremlem  26474  aaliou2  26512  radcnv0  26588  abelthlem2  26604  wilthlem2  27242  vmappw  27289  ppinprm  27325  chtnprm  27327  musumsum  27365  dchrhash  27444  lgsquadlem1  27553  lgsquadlem2  27554  eqcuts3  28006  sltsleft  28062  sltsright  28063  cofcutr  28126  addsuniflem  28203  negsid  28243  negsunif  28257  sltmuls1  28349  sltmuls2  28350  precsexlem11  28419  oncutlt  28466  n0fincut  28557  elreno2  28697  cplgr1v  29789  rusgrnumwwlkb0  30332  frgrncvvdeq  30669  fusgr2wsp2nb  30694  hsn0elch  31609  indsn  33192  cycpmrn  33472  mvrvalind  33937  mplmonprod  33953  esplyfvaln  33973  esplyind  33974  ccfldextdgrr  34071  xrge0iifiso  34334  qqhval2  34381  esumnul  34447  esumrnmpt2  34467  esumfzf  34468  sibfof  34739  sitgaddlemb  34747  signstf0  34964  prodfzo03  34999  circlemeth  35036  scottsn  35528  kard0  35575  sconnpi1  35739  dffr5  36254  elima4  36276  brsingle  36415  dfiota3  36421  funpartfun  36443  dfrdg4  36451  fwddifn0  36664  mh-infprim2bi  37086  mh-infprim3bi  37087  bj-csbsnlem  37566  bj-axsn  37696  bj-axadj  37705  bj-pw0ALT  37713  bj-restsn  37752  bj-rest10  37758  mptsnunlem  38012  fvineqsneu  38085  matunitlindflem1  38295  poimirlem23  38322  poimirlem26  38325  poimirlem27  38326  grposnOLD  38561  0idl  38704  smprngopr  38731  isdmn3  38753  dfsucmap3  39140  ressn2  39209  lshpdisj  39789  lsat0cv  39835  snatpsubN  40552  dibelval3  41949  dib1dim  41967  dvh2dim  42247  mapd0  42467  hdmap14lem13  42682  dvrelogpow2b  42863  sticksstones11  42951  unitscyglem4  42993  sn-iotalem  43020  prjspeclsp  43372  pellexlem5  43588  jm2.23  43751  flcidc  43925  tfsconcatrn  44097  snhesn  44540  snssiALTVD  45563  snssiALT  45564  permaxinf2lem  45749  iccintsng  46267  icoiccdif  46268  limcrecl  46373  lptioo2  46375  lptioo1  46376  limcresiooub  46384  limcresioolb  46385  cnrefiisplem  46571  icccncfext  46629  dvmptfprodlem  46686  dvnprodlem3  46690  dirkercncflem2  46846  fourierdlem40  46889  fourierdlem48  46896  fourierdlem51  46899  fourierdlem62  46910  fourierdlem66  46914  fourierdlem74  46922  fourierdlem75  46923  fourierdlem76  46924  fourierdlem78  46926  fourierdlem79  46927  fourierdlem93  46941  fourierdlem101  46949  fourierdlem103  46951  fourierdlem104  46952  fouriersw  46973  elaa2  46976  etransclem44  47020  rrxsnicc  47042  sge00  47118  chnsubseq  47624  absnsb  47792  funressnfv  47808  fsetsniunop  47814  dfdfat2  47893  tz6.12-afv  47938  tz6.12-afv2  48005  otiunsndisjX  48044  iccpartgtl  48203  iccpartgt  48204  iccpartleu  48205  iccpartgel  48206  nnsum4primeseven  48593  nnsum4primesevenALTV  48594  bgoldbtbnd  48602  dfclnbgr6  48649  dfnbgr6  48650  stgredgiun  48751  xpsnopab  48950  smprngprmrng  49132  isidom3  49138  mo0sn  49622  tposres0  49683  setcsnterm  50296  2arwcatlem1  50401  2arwcat  50406  setc1onsubc  50408  aacllem  50649