Theorem velsn 4664

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

Syntax hints:   ↔ wb 206   = wceq 1537   ∈ wcel 2108  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-sn 4649

This theorem is referenced by:  rabsneq  4666  dfpr2  4668  ralsnsg  4692  rexsns  4693  ralsng  4697  disjsn  4736  snprc  4742  snssb  4807  snssgOLD  4809  raldifsnb  4821  difprsnss  4824  pwpw0  4838  eqsn  4854  eqsndOLD  4856  snsspw  4869  dfnfc2  4953  uni0b  4957  uni0c  4958  iunid  5083  iunsn  5089  sndisj  5158  rext  5468  moabex  5479  exss  5483  otiunsndisj  5539  dffr6  5655  fconstmpt  5762  opeliunxp  5767  rnep  5951  restidsing  6082  xpdifid  6199  dmsnopg  6244  sniota  6564  dfmpt3  6714  nfunsn  6962  fnsnfv  7001  dffv2  7017  fsn  7169  fnasrn  7179  fnsnb  7200  fmptsng  7202  fmptsnd  7203  fvclss  7278  eqfunresadj  7396  eusvobj2  7440  sucexeloniOLD  7846  suceloniOLD  7848  opabex3d  8006  opabex3rd  8007  opabex3  8008  xpord2pred  8186  xpord3pred  8193  frrlem12  8338  frrlem13  8339  wfrlem14OLD  8378  wfrlem15OLD  8379  oarec  8618  mapdm0  8900  ixp0x  8984  snmapen  9103  xpsnen  9121  marypha2lem2  9505  elirrv  9665  cantnfp1lem1  9747  cantnfp1lem3  9749  djuunxp  9990  dfac5lem1  10192  dfac5lem2  10193  dfac5lem4  10195  dfac5lem4OLD  10197  fin1a2lem11  10479  axdc4lem  10524  axcclem  10526  ttukeylem7  10584  xrsupexmnf  13367  xrinfmexpnf  13368  iccid  13452  fzsn  13626  fzpr  13639  seqz  14101  hashf1  14506  pr2pwpr  14528  s3iunsndisj  15017  fsum2dlem  15818  incexc2  15886  prodsn  16010  prodsnf  16012  fprod2dlem  16028  ef0lem  16126  lcmfunsnlem2  16687  1nprm  16726  vdwapun  17021  prmodvdslcmf  17094  cshwsiun  17147  mgmidsssn0  18710  mnd1id  18815  0subm  18852  efmnd1bas  18928  smndex1basss  18940  smndex1mgm  18942  trivsubgsnd  19194  kerf1ghm  19287  ghmqusnsglem1  19320  ghmquskerlem1  19323  ghmqusker  19327  symg1bas  19432  pmtrprfvalrn  19530  gex1  19633  sylow2alem1  19659  lsmdisj2  19724  0frgp  19821  0cyg  19935  prmcyg  19936  dprddisj2  20083  ablfacrp  20110  lspdisj  21150  lidlnz  21275  mulgrhm2  21512  pzriprnglem10  21524  ocvin  21715  psrlidm  22005  mplcoe1  22078  mplcoe5  22081  psdmul  22193  maducoeval2  22667  madugsum  22670  en2top  23013  restsn  23199  ist1-3  23378  ordtt1  23408  cmpcld  23431  unisngl  23556  dissnlocfin  23558  ptopn2  23613  snfil  23893  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALTlem4  24079  haustsms2  24166  tsmsxplem1  24182  tsmsxplem2  24183  ust0  24249  dscopn  24607  nmoid  24784  limcdif  25931  ellimc2  25932  limcmpt  25938  limcres  25941  ply1remlem  26224  plyeq0lem  26269  plyremlem  26364  aaliou2  26400  radcnv0  26477  abelthlem2  26494  wilthlem2  27130  vmappw  27177  ppinprm  27213  chtnprm  27215  musumsum  27253  dchrhash  27333  lgsquadlem1  27442  lgsquadlem2  27443  ssltsn  27855  ssltleft  27927  ssltright  27928  cofcutr  27976  addsuniflem  28052  negsid  28091  negsunif  28105  ssltmul1  28191  ssltmul2  28192  precsexlem11  28259  nohalf  28425  0reno  28447  cplgr1v  29465  rusgrnumwwlkb0  30004  frgrncvvdeq  30341  fusgr2wsp2nb  30366  hsn0elch  31280  cycpmrn  33136  qsxpid  33355  prmidl0  33443  ccfldextdgrr  33682  xrge0iifiso  33881  qqhval2  33928  esumnul  34012  esumrnmpt2  34032  esumfzf  34033  sibfof  34305  sitgaddlemb  34313  plymulx0  34524  signstf0  34545  prodfzo03  34580  circlemeth  34617  sconnpi1  35207  dffr5  35716  elima4  35739  brsingle  35881  dfiota3  35887  funpartfun  35907  dfrdg4  35915  fwddifn0  36128  bj-csbsnlem  36869  bj-axsn  36998  bj-axadj  37007  bj-pw0ALT  37015  bj-restsn  37048  bj-rest10  37054  mptsnunlem  37304  fvineqsneu  37377  matunitlindflem1  37576  poimirlem23  37603  poimirlem26  37606  poimirlem27  37607  grposnOLD  37842  0idl  37985  smprngopr  38012  isdmn3  38034  ressn2  38398  lshpdisj  38943  lsat0cv  38989  snatpsubN  39707  dibelval3  41104  dib1dim  41122  dvh2dim  41402  mapd0  41622  hdmap14lem13  41837  dvrelogpow2b  42025  sticksstones11  42113  unitscyglem4  42155  sn-iotalem  42214  fnsnbt  42225  prjspeclsp  42567  pellexlem5  42789  jm2.23  42953  flcidc  43131  tfsconcatrn  43304  snhesn  43748  snssiALTVD  44798  snssiALT  44799  fsneq  45113  iccintsng  45441  icoiccdif  45442  limcrecl  45550  lptioo2  45552  lptioo1  45553  limcresiooub  45563  limcresioolb  45564  cnrefiisplem  45750  icccncfext  45808  dvmptfprodlem  45865  dvnprodlem3  45869  dirkercncflem2  46025  fourierdlem40  46068  fourierdlem48  46075  fourierdlem51  46078  fourierdlem62  46089  fourierdlem66  46093  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem78  46105  fourierdlem79  46106  fourierdlem93  46120  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  fouriersw  46152  elaa2  46155  etransclem44  46199  rrxsnicc  46221  sge00  46297  absnsb  46942  funressnfv  46958  fsetsniunop  46964  dfdfat2  47043  tz6.12-afv  47088  tz6.12-afv2  47155  otiunsndisjX  47194  iccpartgtl  47300  iccpartgt  47301  iccpartleu  47302  iccpartgel  47303  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  bgoldbtbnd  47683  dfclnbgr6  47728  dfnbgr6  47729  xpsnopab  47880  opeliun2xp  48057  mo0sn  48547  aacllem  48895