Theorem velsn 4646

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

Syntax hints:   ↔ wb 206   = wceq 1536   ∈ wcel 2105  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-sn 4631

This theorem is referenced by:  rabsneq  4648  dfpr2  4650  ralsnsg  4674  rexsns  4675  ralsng  4679  disjsn  4715  snprc  4721  snssb  4786  snssgOLD  4788  raldifsnb  4800  difprsnss  4803  pwpw0  4817  eqsn  4833  eqsndOLD  4835  snsspw  4848  dfnfc2  4933  uni0b  4937  uni0c  4938  iunid  5064  iunsn  5070  sndisj  5139  rext  5458  moabex  5469  exss  5473  otiunsndisj  5529  dffr6  5643  fconstmpt  5750  opeliunxp  5755  rnep  5939  restidsing  6072  xpdifid  6189  dmsnopg  6234  sniota  6553  dfmpt3  6702  nfunsn  6948  fnsnfv  6987  dffv2  7003  fsn  7154  fnasrn  7164  fnsnb  7185  fmptsng  7187  fmptsnd  7188  fvclss  7260  eqfunresadj  7379  eusvobj2  7422  sucexeloniOLD  7829  suceloniOLD  7831  opabex3d  7988  opabex3rd  7989  opabex3  7990  xpord2pred  8168  xpord3pred  8175  frrlem12  8320  frrlem13  8321  wfrlem14OLD  8360  wfrlem15OLD  8361  oarec  8598  mapdm0  8880  ixp0x  8964  snmapen  9076  xpsnen  9093  marypha2lem2  9473  elirrv  9633  cantnfp1lem1  9715  cantnfp1lem3  9717  djuunxp  9958  dfac5lem1  10160  dfac5lem2  10161  dfac5lem4  10163  dfac5lem4OLD  10165  fin1a2lem11  10447  axdc4lem  10492  axcclem  10494  ttukeylem7  10552  xrsupexmnf  13343  xrinfmexpnf  13344  iccid  13428  fzsn  13602  fzpr  13615  seqz  14087  hashf1  14492  pr2pwpr  14514  s3iunsndisj  15003  fsum2dlem  15802  incexc2  15870  prodsn  15994  prodsnf  15996  fprod2dlem  16012  ef0lem  16110  lcmfunsnlem2  16673  1nprm  16712  vdwapun  17007  prmodvdslcmf  17080  cshwsiun  17133  mgmidsssn0  18697  mnd1id  18805  0subm  18842  efmnd1bas  18918  smndex1basss  18930  smndex1mgm  18932  trivsubgsnd  19184  kerf1ghm  19277  ghmqusnsglem1  19310  ghmquskerlem1  19313  ghmqusker  19317  symg1bas  19422  pmtrprfvalrn  19520  gex1  19623  sylow2alem1  19649  lsmdisj2  19714  0frgp  19811  0cyg  19925  prmcyg  19926  dprddisj2  20073  ablfacrp  20100  lspdisj  21144  lidlnz  21269  mulgrhm2  21506  pzriprnglem10  21518  ocvin  21709  psrlidm  21999  mplcoe1  22072  mplcoe5  22075  psdmul  22187  maducoeval2  22661  madugsum  22664  en2top  23007  restsn  23193  ist1-3  23372  ordtt1  23402  cmpcld  23425  unisngl  23550  dissnlocfin  23552  ptopn2  23607  snfil  23887  alexsubALTlem2  24071  alexsubALTlem3  24072  alexsubALTlem4  24073  haustsms2  24160  tsmsxplem1  24176  tsmsxplem2  24177  ust0  24243  dscopn  24601  nmoid  24778  limcdif  25925  ellimc2  25926  limcmpt  25932  limcres  25935  ply1remlem  26218  plyeq0lem  26263  plyremlem  26360  aaliou2  26396  radcnv0  26473  abelthlem2  26490  wilthlem2  27126  vmappw  27173  ppinprm  27209  chtnprm  27211  musumsum  27249  dchrhash  27329  lgsquadlem1  27438  lgsquadlem2  27439  ssltsn  27851  ssltleft  27923  ssltright  27924  cofcutr  27972  addsuniflem  28048  negsid  28087  negsunif  28101  ssltmul1  28187  ssltmul2  28188  precsexlem11  28255  nohalf  28421  0reno  28443  cplgr1v  29461  rusgrnumwwlkb0  30000  frgrncvvdeq  30337  fusgr2wsp2nb  30362  hsn0elch  31276  cycpmrn  33145  qsxpid  33369  prmidl0  33457  ccfldextdgrr  33696  xrge0iifiso  33895  qqhval2  33944  esumnul  34028  esumrnmpt2  34048  esumfzf  34049  sibfof  34321  sitgaddlemb  34329  plymulx0  34540  signstf0  34561  prodfzo03  34596  circlemeth  34633  sconnpi1  35223  dffr5  35733  elima4  35756  brsingle  35898  dfiota3  35904  funpartfun  35924  dfrdg4  35932  fwddifn0  36145  bj-csbsnlem  36885  bj-axsn  37014  bj-axadj  37023  bj-pw0ALT  37031  bj-restsn  37064  bj-rest10  37070  mptsnunlem  37320  fvineqsneu  37393  matunitlindflem1  37602  poimirlem23  37629  poimirlem26  37632  poimirlem27  37633  grposnOLD  37868  0idl  38011  smprngopr  38038  isdmn3  38060  ressn2  38423  lshpdisj  38968  lsat0cv  39014  snatpsubN  39732  dibelval3  41129  dib1dim  41147  dvh2dim  41427  mapd0  41647  hdmap14lem13  41862  dvrelogpow2b  42049  sticksstones11  42137  unitscyglem4  42179  sn-iotalem  42238  fnsnbt  42249  prjspeclsp  42598  pellexlem5  42820  jm2.23  42984  flcidc  43158  tfsconcatrn  43331  snhesn  43775  snssiALTVD  44824  snssiALT  44825  fsneq  45148  iccintsng  45475  icoiccdif  45476  limcrecl  45584  lptioo2  45586  lptioo1  45587  limcresiooub  45597  limcresioolb  45598  cnrefiisplem  45784  icccncfext  45842  dvmptfprodlem  45899  dvnprodlem3  45903  dirkercncflem2  46059  fourierdlem40  46102  fourierdlem48  46109  fourierdlem51  46112  fourierdlem62  46123  fourierdlem66  46127  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem78  46139  fourierdlem79  46140  fourierdlem93  46154  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  fouriersw  46186  elaa2  46189  etransclem44  46233  rrxsnicc  46255  sge00  46331  absnsb  46976  funressnfv  46992  fsetsniunop  46998  dfdfat2  47077  tz6.12-afv  47122  tz6.12-afv2  47189  otiunsndisjX  47228  iccpartgtl  47350  iccpartgt  47351  iccpartleu  47352  iccpartgel  47353  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  bgoldbtbnd  47733  dfclnbgr6  47779  dfnbgr6  47780  stgredgiun  47860  xpsnopab  48000  opeliun2xp  48177  mo0sn  48663  aacllem  49031