Theorem velsn 4598

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {csn 4582

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-sn 4583

This theorem is referenced by:  rabsneq  4601  dfpr2  4603  ralsnsg  4629  rexsns  4630  ralsng  4634  disjsn  4670  snprc  4676  snssb  4741  raldifsnb  4754  difprsnss  4757  pwpw0  4771  eqsn  4787  eqsndOLD  4789  snsspw  4802  dfnfc2  4887  uni0b  4891  uni0c  4892  iunid  5018  iunsn  5023  sndisj  5092  rext  5405  moabexOLD  5416  exss  5420  otiunsndisj  5478  dffr6  5590  fconstmpt  5696  opeliunxp  5701  opeliun2xp  5702  rnep  5886  restidsing  6022  xpdifid  6136  dmsnopg  6181  sniota  6493  dfmpt3  6636  tz6.12-2  6831  nfunsn  6883  fnsnfv  6923  dffv2  6939  fsn  7092  fnasrn  7102  fnsnbg  7122  fnsnbOLD  7124  fmptsng  7126  fmptsnd  7127  fvclss  7199  eqfunresadj  7318  eusvobj2  7362  resf1extb  7888  opabex3d  7921  opabex3rd  7922  opabex3  7923  xpord2pred  8099  xpord3pred  8106  frrlem12  8251  frrlem13  8252  oarec  8501  mapdm0  8793  ixp0x  8878  snmapen  8989  xpsnen  9003  marypha2lem2  9353  elirrvOLD  9517  cantnfp1lem1  9601  cantnfp1lem3  9603  djuunxp  9847  dfac5lem1  10047  dfac5lem2  10048  dfac5lem4  10050  dfac5lem4OLD  10052  fin1a2lem11  10334  axdc4lem  10379  axcclem  10381  ttukeylem7  10439  xrsupexmnf  13234  xrinfmexpnf  13235  iccid  13320  fzsn  13496  fzpr  13509  seqz  13987  hashf1  14394  pr2pwpr  14416  s3iunsndisj  14905  fsum2dlem  15707  incexc2  15775  prodsn  15899  prodsnf  15901  fprod2dlem  15917  ef0lem  16015  lcmfunsnlem2  16581  1nprm  16620  vdwapun  16916  prmodvdslcmf  16989  cshwsiun  17041  chnccat  18563  mgmidsssn0  18611  mnd1id  18719  0subm  18756  efmnd1bas  18832  smndex1basss  18847  smndex1mgm  18849  trivsubgsnd  19100  kerf1ghm  19193  ghmqusnsglem1  19226  ghmquskerlem1  19229  ghmqusker  19233  symg1bas  19337  pmtrprfvalrn  19434  gex1  19537  sylow2alem1  19563  lsmdisj2  19628  0frgp  19725  0cyg  19839  prmcyg  19840  dprddisj2  19987  ablfacrp  20014  lspdisj  21097  lidlnz  21214  mulgrhm2  21450  pzriprnglem10  21462  ocvin  21646  psrlidm  21934  mplcoe1  22009  mplcoe5  22012  psdmul  22126  maducoeval2  22601  madugsum  22604  en2top  22946  restsn  23131  ist1-3  23310  ordtt1  23340  cmpcld  23363  unisngl  23488  dissnlocfin  23490  ptopn2  23545  snfil  23825  alexsubALTlem2  24009  alexsubALTlem3  24010  alexsubALTlem4  24011  haustsms2  24098  tsmsxplem1  24114  tsmsxplem2  24115  ust0  24181  dscopn  24534  nmoid  24703  limcdif  25850  ellimc2  25851  limcmpt  25857  limcres  25860  ply1remlem  26143  plyeq0lem  26188  plyremlem  26285  aaliou2  26321  radcnv0  26398  abelthlem2  26415  wilthlem2  27052  vmappw  27099  ppinprm  27135  chtnprm  27137  musumsum  27175  dchrhash  27255  lgsquadlem1  27364  lgsquadlem2  27365  eqcuts3  27817  sltsleft  27873  sltsright  27874  cofcutr  27937  addsuniflem  28014  negsid  28054  negsunif  28068  sltmuls1  28160  sltmuls2  28161  precsexlem11  28230  oncutlt  28277  n0fincut  28368  elreno2  28508  cplgr1v  29521  rusgrnumwwlkb0  30065  frgrncvvdeq  30402  fusgr2wsp2nb  30427  hsn0elch  31342  indsn  32962  cycpmrn  33243  qsxpid  33461  prmidl0  33549  mvrvalind  33721  mplmonprod  33737  esplyfvaln  33757  esplyind  33758  ccfldextdgrr  33856  xrge0iifiso  34119  qqhval2  34166  esumnul  34232  esumrnmpt2  34252  esumfzf  34253  sibfof  34524  sitgaddlemb  34532  plymulx0  34731  signstf0  34752  prodfzo03  34787  circlemeth  34824  sconnpi1  35461  dffr5  35976  elima4  35998  brsingle  36137  dfiota3  36143  funpartfun  36165  dfrdg4  36173  fwddifn0  36386  bj-csbsnlem  37178  bj-axsn  37307  bj-axadj  37316  bj-pw0ALT  37324  bj-restsn  37362  bj-rest10  37368  mptsnunlem  37620  fvineqsneu  37693  matunitlindflem1  37896  poimirlem23  37923  poimirlem26  37926  poimirlem27  37927  grposnOLD  38162  0idl  38305  smprngopr  38332  isdmn3  38354  dfsucmap3  38743  ressn2  38812  lshpdisj  39392  lsat0cv  39438  snatpsubN  40155  dibelval3  41552  dib1dim  41570  dvh2dim  41850  mapd0  42070  hdmap14lem13  42285  dvrelogpow2b  42467  sticksstones11  42555  unitscyglem4  42597  sn-iotalem  42622  prjspeclsp  42999  pellexlem5  43219  jm2.23  43382  flcidc  43556  tfsconcatrn  43728  snhesn  44171  snssiALTVD  45211  snssiALT  45212  permaxinf2lem  45397  fsneq  45593  iccintsng  45912  icoiccdif  45913  limcrecl  46018  lptioo2  46020  lptioo1  46021  limcresiooub  46029  limcresioolb  46030  cnrefiisplem  46216  icccncfext  46274  dvmptfprodlem  46331  dvnprodlem3  46335  dirkercncflem2  46491  fourierdlem40  46534  fourierdlem48  46541  fourierdlem51  46544  fourierdlem62  46555  fourierdlem66  46559  fourierdlem74  46567  fourierdlem75  46568  fourierdlem76  46569  fourierdlem78  46571  fourierdlem79  46572  fourierdlem93  46586  fourierdlem101  46594  fourierdlem103  46596  fourierdlem104  46597  fouriersw  46618  elaa2  46621  etransclem44  46665  rrxsnicc  46687  sge00  46763  chnsubseq  47267  absnsb  47416  funressnfv  47432  fsetsniunop  47438  dfdfat2  47517  tz6.12-afv  47562  tz6.12-afv2  47629  otiunsndisjX  47668  iccpartgtl  47815  iccpartgt  47816  iccpartleu  47817  iccpartgel  47818  nnsum4primeseven  48189  nnsum4primesevenALTV  48190  bgoldbtbnd  48198  dfclnbgr6  48245  dfnbgr6  48246  stgredgiun  48347  xpsnopab  48546  mo0sn  49204  tposres0  49265  setcsnterm  49878  2arwcatlem1  49983  2arwcat  49988  setc1onsubc  49990  aacllem  50189