Theorem velsn 4600

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

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

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-sn 4585

This theorem is used by:  rabsneq  4603  dfpr2  4605  ralsnsg  4631  rexsns  4632  ralsng  4636  disjsn  4672  snprc  4678  snssb  4743  raldifsnb  4759  difprsnss  4762  pwpw0  4774  eqsn  4790  snsspw  4804  dfnfc2  4889  uni0b  4894  uni0c  4895  iunid  5019  iunsn  5024  rext  5423  moabexOLD  5434  exss  5438  otiunsndisj  5497  dffr6  5611  fconstmpt  5717  opeliunxp  5722  opeliun2xp  5723  rnep  5913  restidsing  6051  xpdifid  6162  dmsnopg  6211  sniota  6526  dfmpt3  6669  tz6.12-2  6868  nfunsn  6920  fnsnfv  6960  dffv2  6976  fsneq  7030  fsn  7132  fnasrn  7144  fnsnbg  7165  fnsnbOLD  7167  fmptsng  7169  fmptsnd  7170  fvclss  7241  eqfunresadj  7366  eusvobj2  7408  resf1extb  7937  opabex3d  7968  opabex3rd  7969  opabex3  7970  xpord2pred  8148  xpord3pred  8155  frrlem12  8301  frrlem13  8302  oarec  8556  mapdm0  8848  ixp0x  8940  snmapen  9052  xpsnen  9066  marypha2lem2  9413  elirrvOLDOLD  9578  cantnfp1lem1  9664  cantnfp1lem3  9666  djuunxp  9951  dfac5lem1  10151  dfac5lem2  10152  dfac5lem4  10154  fin1a2lem11  10437  axdc4lem  10482  axcclem  10484  ttukeylem7  10542  xrsupexmnf  13382  xrinfmexpnf  13383  iccid  13468  fzsn  13646  fzpr  13659  seqz  14139  hashf1  14547  pr2pwpr  14569  s3iunsndisj  15066  fsum2dlem  15881  incexc2  15952  prodsn  16074  prodsnf  16076  fprod2dlem  16092  ef0lem  16189  lcmfunsnlem2  16755  1nprm  16794  vdwapun  17091  prmodvdslcmf  17164  cshwsiun  17216  chnccat  18739  mgmidsssn0  18792  mnd1id  18913  0subm  18952  efmnd1bas  19028  smndex1basss  19043  smndex1mgm  19045  trivsubgsnd  19303  qsxpid  19326  kerf1ghm  19400  ghmqusnsglem1  19433  ghmquskerlem1  19436  ghmqusker  19440  symg1bas  19544  pmtrprfvalrn  19641  gex1  19744  sylow2alem1  19770  lsmdisj2  19835  0frgp  19932  0cyg  20046  prmcyg  20047  dprddisj2  20194  ablfacrp  20221  lspdisj  21342  lidlnz  21469  prmidl0  21573  mulgrhm2  21723  pzriprnglem10  21735  ocvin  21919  psrlidm  22208  mplcoe1  22285  mplcoe5  22288  psdmul  22426  maducoeval2  22894  madugsum  22897  matunitlindflem1  22933  en2top  23242  restsn  23427  ist1-3  23606  ordtt1  23636  cmpcld  23659  unisngl  23785  dissnlocfin  23787  ptopn2  23842  snfil  24122  alexsubALTlem2  24306  alexsubALTlem3  24307  alexsubALTlem4  24308  haustsms2  24395  tsmsxplem1  24411  tsmsxplem2  24412  ust0  24478  dscopn  24831  nmoid  25000  limcdif  26135  ellimc2  26136  limcmpt  26142  limcres  26145  ply1remlem  26422  plyeq0lem  26468  plyn0mulidp  26543  plyremlem  26566  aaliou2  26608  radcnv0  26684  abelthlem2  26700  wilthlem2  27337  vmappw  27384  ppinprm  27420  chtnprm  27422  musumsum  27460  dchrhash  27539  lgsquadlem1  27648  lgsquadlem2  27649  eqcuts3  28101  sltsleft  28157  sltsright  28158  cofcutr  28221  addsuniflem  28298  negsid  28338  negsunif  28352  sltmuls1  28444  sltmuls2  28445  precsexlem11  28514  oncutlt  28561  n0fincut  28652  elreno2  28792  cplgr1v  29922  rusgrnumwwlkb0  30474  frgrncvvdeq  30821  fusgr2wsp2nb  30846  hsn0elch  31761  indsn  33341  cycpmrn  33615  mvrvalind  34081  mplmonprod  34097  esplyfvaln  34117  esplyind  34118  ccfldextdgrr  34215  xrge0iifiso  34478  qqhval2  34525  esumnul  34591  esumrnmpt2  34611  esumfzf  34612  sibfof  34884  sitgaddlemb  34892  signstf0  35109  prodfzo03  35144  circlemeth  35181  scottsn  35666  kard0  35723  sconnpi1  35901  elima4  36438  brsingle  36577  dfiota3  36583  funpartfun  36605  dfrdg4  36613  fwddifn0  36827  mh-infprim2bi  37233  mh-infprim3bi  37234  bj-csbsnlem  37713  bj-axsn  37843  bj-axadj  37852  bj-pw0ALT  37860  bj-restsn  37899  bj-rest10  37905  mptsnunlem  38157  fvineqsneu  38230  poimirlem23  38457  poimirlem26  38460  poimirlem27  38461  grposnOLD  38697  0idl  38840  smprngopr  38867  isdmn3  38889  dfsucmap3  39276  ressn2  39345  lshpdisj  39925  lsat0cv  39971  snatpsubN  40688  dibelval3  42085  dib1dim  42103  dvh2dim  42383  mapd0  42603  hdmap14lem13  42818  dvrelogpow2b  42999  sticksstones11  43087  unitscyglem4  43129  sn-iotalem  43156  prjspeclsp  43523  pellexlem5  43739  jm2.23  43902  flcidc  44076  tfsconcatrn  44248  snhesn  44691  snssiALTVD  45714  snssiALT  45715  permaxinf2lem  45900  iccintsng  46418  icoiccdif  46419  limcrecl  46524  lptioo2  46526  lptioo1  46527  limcresiooub  46535  limcresioolb  46536  cnrefiisplem  46722  icccncfext  46780  dvmptfprodlem  46837  dvnprodlem3  46841  dirkercncflem2  46997  fourierdlem40  47040  fourierdlem48  47047  fourierdlem51  47050  fourierdlem62  47061  fourierdlem66  47065  fourierdlem74  47073  fourierdlem75  47074  fourierdlem76  47075  fourierdlem78  47077  fourierdlem79  47078  fourierdlem93  47092  fourierdlem101  47100  fourierdlem103  47102  fourierdlem104  47103  fouriersw  47124  elaa2  47127  etransclem44  47171  rrxsnicc  47193  sge00  47269  absnsb  47980  funressnfv  47996  fsetsniunop  48002  dfdfat2  48081  tz6.12-afv  48126  tz6.12-afv2  48193  otiunsndisjX  48232  iccpartgtl  48391  iccpartgt  48392  iccpartleu  48393  iccpartgel  48394  nnsum4primeseven  48781  nnsum4primesevenALTV  48782  bgoldbtbnd  48790  dfclnbgr6  48837  dfnbgr6  48838  stgredgiun  48939  xpsnopab  49138  smprngprmrng  49319  isidom3  49325  mo0sn  49809  tposres0  49868  setcsnterm  50481  2arwcatlem1  50586  2arwcat  50591  setc1onsubc  50593  aacllem  50837