Theorem velsn 4541

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

Syntax hints:   ↔ wb 209   = wceq 1538   ∈ wcel 2111  {csn 4525

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-sn 4526

This theorem is referenced by:  dfpr2  4544  ralsnsg  4568  rexsns  4569  disjsn  4607  snprc  4613  snssg  4678  raldifsnb  4689  difprsnss  4692  pwpw0  4706  eqsn  4722  snsspw  4735  pwsnOLD  4793  dfnfc2  4822  uni0b  4826  uni0c  4827  sndisj  5021  rext  5306  moabex  5316  exss  5320  otiunsndisj  5375  fconstmpt  5578  opeliunxp  5583  rnep  5761  restidsing  5889  xpdifid  5992  dmsnopg  6037  sniota  6315  dfmpt3  6454  nfunsn  6682  dffv2  6733  fsn  6874  fnasrn  6884  fnsnb  6905  fmptsng  6907  fmptsnd  6908  fvclss  6979  eusvobj2  7128  suceloni  7508  opabex3d  7648  opabex3rd  7649  opabex3  7650  wfrlem14  7951  wfrlem15  7952  oarec  8171  mapdm0  8404  ixp0x  8473  snmapen  8573  xpsnen  8584  marypha2lem2  8884  elirrv  9044  cantnfp1lem1  9125  cantnfp1lem3  9127  djuunxp  9334  dfac5lem1  9534  dfac5lem2  9535  dfac5lem4  9537  fin1a2lem11  9821  axdc4lem  9866  axcclem  9868  ttukeylem7  9926  xrsupexmnf  12686  xrinfmexpnf  12687  iccid  12771  fzsn  12944  fzpr  12957  seqz  13414  hashf1  13811  pr2pwpr  13833  s3iunsndisj  14319  fsum2dlem  15117  incexc2  15185  prodsn  15308  prodsnf  15310  fprod2dlem  15326  ef0lem  15424  lcmfunsnlem2  15974  1nprm  16013  vdwapun  16300  prmodvdslcmf  16373  cshwsiun  16425  mgmidsssn0  17874  mnd1id  17945  0subm  17974  efmnd1bas  18050  smndex1basss  18062  smndex1mgm  18064  trivsubgsnd  18298  symg1bas  18511  pmtrprfvalrn  18608  gex1  18708  sylow2alem1  18734  lsmdisj2  18800  0frgp  18897  0cyg  19006  prmcyg  19007  dprddisj2  19154  ablfacrp  19181  kerf1ghm  19491  lspdisj  19890  lidlnz  19994  mulgrhm2  20192  ocvin  20363  psrlidm  20641  mplcoe1  20705  mplcoe5  20708  maducoeval2  21245  madugsum  21248  en2top  21590  restsn  21775  ist1-3  21954  ordtt1  21984  cmpcld  22007  unisngl  22132  dissnlocfin  22134  ptopn2  22189  snfil  22469  alexsubALTlem2  22653  alexsubALTlem3  22654  alexsubALTlem4  22655  haustsms2  22742  tsmsxplem1  22758  tsmsxplem2  22759  ust0  22825  dscopn  23180  nmoid  23348  limcdif  24479  ellimc2  24480  limcmpt  24486  limcres  24489  ply1remlem  24763  plyeq0lem  24807  plyremlem  24900  aaliou2  24936  radcnv0  25011  abelthlem2  25027  wilthlem2  25654  vmappw  25701  ppinprm  25737  chtnprm  25739  musumsum  25777  dchrhash  25855  lgsquadlem1  25964  lgsquadlem2  25965  cplgr1v  27220  rusgrnumwwlkb0  27757  frgrncvvdeq  28094  fusgr2wsp2nb  28119  hsn0elch  29031  eqsnd  30301  cycpmrn  30835  qsxpid  30978  prmidl0  31034  ccfldextdgrr  31145  xrge0iifiso  31288  qqhval2  31333  esumnul  31417  esumrnmpt2  31437  esumfzf  31438  sibfof  31708  sitgaddlemb  31716  plymulx0  31927  signstf0  31948  prodfzo03  31984  circlemeth  32021  bnj521  32117  sconnpi1  32599  dffr5  33102  eqfunresadj  33117  elima4  33132  frrlem12  33247  frrlem13  33248  brsingle  33491  dfiota3  33497  funpartfun  33517  dfrdg4  33525  fwddifn0  33738  bj-csbsnlem  34344  bj-pw0ALT  34466  bj-restsn  34497  bj-rest10  34503  mptsnunlem  34755  fvineqsneu  34828  matunitlindflem1  35053  poimirlem23  35080  poimirlem26  35083  poimirlem27  35084  grposnOLD  35320  0idl  35463  smprngopr  35490  isdmn3  35512  lshpdisj  36283  lsat0cv  36329  snatpsubN  37046  dibelval3  38443  dib1dim  38461  dvh2dim  38741  mapd0  38961  hdmap14lem13  39176  iunsn  39412  fnsnbt  39414  prjspeclsp  39606  pellexlem5  39774  jm2.23  39937  flcidc  40118  snhesn  40487  snssiALTVD  41533  snssiALT  41534  fsneq  41835  iccintsng  42160  icoiccdif  42161  limcrecl  42271  lptioo2  42273  lptioo1  42274  limcresiooub  42284  limcresioolb  42285  cnrefiisplem  42471  icccncfext  42529  dvmptfprodlem  42586  dvnprodlem3  42590  dirkercncflem2  42746  fourierdlem40  42789  fourierdlem48  42796  fourierdlem51  42799  fourierdlem62  42810  fourierdlem66  42814  fourierdlem74  42822  fourierdlem75  42823  fourierdlem76  42824  fourierdlem78  42826  fourierdlem79  42827  fourierdlem93  42841  fourierdlem101  42849  fourierdlem103  42851  fourierdlem104  42852  fouriersw  42873  elaa2  42876  etransclem44  42920  rrxsnicc  42942  sge00  43015  absnsb  43619  funressnfv  43635  dfdfat2  43684  tz6.12-afv  43729  tz6.12-afv2  43796  otiunsndisjX  43835  iccpartgtl  43943  iccpartgt  43944  iccpartleu  43945  iccpartgel  43946  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  bgoldbtbnd  44327  xpsnopab  44385  opeliun2xp  44734  aacllem  45329