Theorem snex 5410

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation and Pairing. See also snexALT 5354. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) Avoid ax-nul 5269 and shorten proof. (Revised by GG, 6-Mar-2026.)

Assertion

Ref	Expression
snex	⊢ {𝐴} ∈ V

Proof of Theorem snex

Step	Hyp	Ref	Expression
1		dfsn2 4602	. 2 ⊢ {𝐴} = {𝐴, 𝐴}
2		prex 5409	. 2 ⊢ {𝐴, 𝐴} ∈ V
3	1, 2	eqeltri 2859	1 ⊢ {𝐴} ∈ V

Syntax hints:   ∈ wcel 2143  Vcvv 3455  {csn 4589  {cpr 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-sn 4590  df-pr 4592

This theorem is referenced by:  snexg  5411  elopg  5448  opi1  5450  op1stb  5453  opnz  5455  opeqsng  5486  opeqpr  5488  snopeqop  5489  opthwiener  5497  uniop  5498  0sn0ep  5565  frirr  5637  opthprc  5725  frsn  5749  relop  5836  snsn0non  6487  onnev  6489  funsneqopb  7149  fsnex  7281  tpex  7743  difsnexi  7756  sucexb  7799  elxp4  7915  elxp5  7916  fvclex  7952  1stval  7984  2ndval  7985  fnse  8125  suppsnop  8170  brtpos2  8224  frrlem13  8291  tfrlem12  8372  tfrlem16  8376  1oex  8459  naddunif  8676  mapsnd  8880  fvdiagfn  8885  mapsnconst  8886  mapsncnv  8887  mapsnf1o2  8888  ralxpmap  8890  elixpsn  8931  ixpsnf1o  8932  mapsnf1o  8933  ensn1  9014  2dom  9023  mapsnend  9029  snmapen  9031  en2sn  9034  xpsnen  9045  endisj  9048  xpsnen2g  9054  domunsncan  9061  enfixsn  9070  disjenex  9119  domssex2  9121  domssex  9122  map2xp  9131  pssnn  9149  snnen2o  9201  isinf  9221  ac6sfi  9240  fczfsuppd  9342  snopfsupp  9347  fisn  9383  tc2  9705  tcsni  9706  ranksuc  9833  djuex  9890  fseqenlem1  10004  djuassen  10158  mapdjuen  10160  djudom1  10162  djuinf  10168  ackbij1lem5  10202  cfsuc  10236  dcomex  10426  axdc3lem4  10432  axdc4lem  10434  ttukeylem3  10490  brdom7disj  10510  brdom6disj  10511  fpwwe2lem12  10622  nn0ex  12505  hashxplem  14466  hashf1lem1  14488  hashge3el3dif  14520  ofs1  15003  climconst2  15595  ramub1lem2  17082  cshwsex  17155  setsvalg  17221  setsid  17262  pwsbas  17535  pwsle  17541  pwssca  17545  pwssnf1o  17547  imasplusg  17566  imasmulr  17567  imasvsca  17569  imasip  17570  acsfn  17710  homaval  18083  funcsetcestrclem1  18205  mgm1  18711  sgrp1  18782  mnd1  18832  mnd1id  18833  efmnd1bas  18947  idresefmnd  18953  smndex1gbas  18956  smndex1gid  18958  smndex1igid  18960  smndex1bas  18963  smndex1sgrp  18965  smndex1mnd  18967  smndex1id  18968  grp1  19108  grp1inv  19109  mulgfval  19130  triv1nsgd  19234  1nsgtrivd  19235  symg2bas  19458  idrespermg  19476  pmtrsn  19584  psgnsn  19585  abl1  19931  dprdz  20097  dprdsn  20103  simpgnsgd  20167  2nsgsimpgd  20169  ring1  20389  rng1nnzr  20879  pwssplit3  21182  lpival  21492  cnfldex  21525  pzriprnglem13  21643  pzriprnglem14  21644  frlmip  21928  islindf4  21988  evlsvvval  22244  evlssca  22245  evlsevl  22283  psdmul  22329  evls1sca  22483  mattposvs  22612  mat1dimelbas  22628  mat1dimscm  22632  mat1dimmul  22633  mat1rhmval  22636  m1detdiag  22754  mdetrlin  22759  mdetrsca2  22761  mdetrlin2  22764  mdetunilem5  22773  smadiadetglem2  22829  basdif0  23110  ordtbas  23349  leordtval2  23369  conncompid  23588  ptbasfi  23738  dfac14lem  23774  dfac14  23775  ptrescn  23796  xkoptsub  23811  pt1hmeo  23963  xpstopnlem1  23966  ufileu  24076  filufint  24077  uffix  24078  uffixsn  24082  flimclslem  24141  ptcmplem1  24209  imasdsf1olem  24530  icccmplem1  24980  icccmplem2  24981  rrxip  25549  rrxsca  25555  ehl1eudis  25579  elply2  26353  plyss  26356  plyeq0lem  26367  taylfval  26522  sltssnb  27962  lesrec  27992  eqcuts3  27997  0lt1s  28005  sltsleft  28053  sltsright  28054  addsval  28155  addsuniflem  28194  negsid  28234  negsunif  28248  mulsval  28302  sltmuls1  28340  sltmuls2  28341  precsexlem1  28400  precsexlem2  28401  precsexlem11  28410  n0fincut  28548  axlowdimlem15  29306  axlowdim  29311  snstriedgval  29388  vtxvalsnop  29391  iedgvalsnop  29392  upgr1eop  29465  upgr1eopALT  29467  uspgr1eop  29597  usgr1eop  29600  1loopgrvd2  29853  1loopgrvd0  29854  p1evtxdeqlem  29862  p1evtxdeq  29863  p1evtxdp1  29864  uspgrloopvtx  29865  uspgrloopiedg  29867  uspgrloopedg  29868  wlkp1lem4  30024  0pthonv  30480  eupth2lem3  30587  wlkl0  30718  0ofval  31139  suppovss  33026  padct  33063  resf1o  33075  elrgspnlem4  33565  elrspunsn  33737  drngidlhash  33741  fldlring  33789  0mplrim  33904  selvply1rhmlema  33908  selvply1rhmlemb  33909  selvply1rhmlem1  33910  selvply1rhmlem2  33911  selvply1rhmlem4  33913  zar0ring  34268  ordtconnlem1  34314  esumpr  34456  esumrnmpt2  34458  esumfzf  34459  prsiga  34521  rossros  34570  cntnevol  34618  omsmeas  34713  ccatmulgnn0dir  34932  ofcs1  34934  actfunsnf1o  34991  actfunsnrndisj  34992  reprsuc  35002  breprexplema  35017  bnj918  35155  bnj95  35252  bnj1489  35444  fineqvac  35529  kard0  35567  kardsn  35573  subfacp1lem5  35676  erdszelem5  35687  erdszelem8  35690  cvmliftlem4  35780  cvmliftlem5  35781  cvmlift2lem6  35800  cvmlift2lem9  35803  cvmlift2lem12  35806  satfv1lem  35854  prv1n  35923  brapply  36428  lemsuccf  36431  altopthsn  36453  hfsn  36671  neibastop2lem  36871  topjoin  36876  onpsstopbas  36941  weiunse  36979  ttcsnexg  37031  bj-2uplex  37658  bj-restsn  37724  finixpnum  38256  ptrest  38270  poimirlem3  38274  poimirlem4  38275  poimirlem28  38299  fdc  38396  heiborlem8  38469  ismrer1  38489  grposnOLD  38533  zrdivrng  38604  lsatset  39764  ldualset  39899  lineset  40512  dvaset  41779  dvhset  41855  dibval  41916  dibfna  41928  sticksstones9  42921  frlmsnic  43308  elrfi  43425  wopprc  43757  dfac11  43789  kelac2  43792  safesnsupfidom1o  44143  sn1dom  44252  pr2dom  44253  tr3dom  44254  fvilbdRP  44416  brtrclfv2  44453  frege110  44699  frege133  44722  k0004lem3  44875  mnuprdlem1  44982  mnuprdlem2  44983  mnuprdlem3  44984  snelpwrVD  45539  nregmodelf1o  45724  fnchoice  45749  elmapsnd  45921  difmapsn  45928  unirnmapsn  45930  ssmapsn  45932  limcresiooub  46356  limcresioolb  46357  cnfdmsn  46596  dvsinax  46627  fourierdlem48  46868  fourierdlem49  46869  sge0sn  47093  sge0p1  47128  hoicvr  47262  ovnovollem1  47370  ovnovollem2  47371  vonvolmbllem  47374  nthrucw  47607  fsetsnf  47788  fsetsnf1  47789  fsetsnfo  47790  cfsetsnfsetfo  47797  setsv  48127  nnsum3primesprm  48555  mapsnop  49124  lindsrng01  49248  snlindsntorlem  49250  snlindsntor  49251  lmod1lem1  49267  lmod1lem2  49268  lmod1lem3  49269  lmod1lem4  49270  lmod1lem5  49271  lmod1  49272  lmod1zr  49273  fv1arycl  49417  1arympt1fv  49419  1arymaptfo  49423  eufsn2  49621  discsubclem  49841  discsubc  49842  iinfconstbas  49844  diag1f1lem  50084  setcsnterm  50268  setc1ocofval  50272  isinito2lem  50276  idfudiag1  50303  diag1f1olem  50311  prstchomval  50337  mndtcbasval  50358  mndtchom  50362  mndtcco  50363  incat  50379  setc1onsubc  50380  aacllem  50621