Theorem snex 5368

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

Assertion

Ref	Expression
snex	⊢ {𝐴} ∈ V

Proof of Theorem snex

Step	Hyp	Ref	Expression
1		dfsn2 4568	. 2 ⊢ {𝐴} = {𝐴, 𝐴}
2		prex 5367	. 2 ⊢ {𝐴, 𝐴} ∈ V
3	1, 2	eqeltri 2835	1 ⊢ {𝐴} ∈ V

Syntax hints:   ∈ wcel 2119  Vcvv 3431  {csn 4555  {cpr 4557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-sn 4556  df-pr 4558

This theorem is referenced by:  snexg  5369  elopg  5406  opi1  5408  op1stb  5411  opnz  5413  opeqsng  5444  opeqpr  5446  snopeqop  5447  opthwiener  5455  uniop  5456  0sn0ep  5522  frirr  5594  opthprc  5682  frsn  5706  relop  5792  snsn0non  6436  onnev  6438  funsneqopb  7095  fsnex  7227  tpex  7689  difsnexi  7704  sucexb  7747  elxp4  7862  elxp5  7863  fvclex  7901  1stval  7933  2ndval  7934  fnse  8073  suppsnop  8118  brtpos2  8172  frrlem13  8238  tfrlem12  8318  tfrlem16  8322  1oex  8405  naddunif  8619  mapsnd  8824  fvdiagfn  8829  mapsnconst  8830  mapsncnv  8831  mapsnf1o2  8832  ralxpmap  8834  elixpsn  8875  ixpsnf1o  8876  mapsnf1o  8877  ensn1  8958  2dom  8967  mapsnend  8973  snmapen  8975  en2sn  8978  xpsnen  8989  endisj  8992  xpsnen2g  8998  domunsncan  9005  enfixsn  9014  disjenex  9063  domssex2  9065  domssex  9066  map2xp  9075  pssnn  9093  snnen2o  9145  isinf  9165  ac6sfi  9184  fodomfiOLD  9230  fczfsuppd  9289  snopfsupp  9294  fisn  9330  tc2  9652  tcsni  9653  ranksuc  9780  djuex  9823  fseqenlem1  9937  djuassen  10092  mapdjuen  10094  djudom1  10096  djuinf  10102  ackbij1lem5  10136  cfsuc  10170  dcomex  10360  axdc3lem4  10366  axdc4lem  10368  ttukeylem3  10424  brdom7disj  10444  brdom6disj  10445  fpwwe2lem12  10556  nn0ex  12434  hashxplem  14386  hashf1lem1  14408  hashge3el3dif  14440  ofs1  14923  climconst2  15501  ramub1lem2  16989  cshwsex  17062  setsvalg  17127  setsid  17168  pwsbas  17441  pwsle  17447  pwssca  17451  pwssnf1o  17453  imasplusg  17472  imasmulr  17473  imasvsca  17475  imasip  17476  acsfn  17616  homaval  17989  funcsetcestrclem1  18111  mgm1  18617  sgrp1  18688  mnd1  18738  mnd1id  18739  efmnd1bas  18852  idresefmnd  18858  smndex1gbas  18861  smndex1gid  18863  smndex1igid  18865  smndex1bas  18868  smndex1sgrp  18870  smndex1mnd  18872  smndex1id  18873  grp1  19014  grp1inv  19015  mulgfval  19036  triv1nsgd  19139  1nsgtrivd  19140  symg2bas  19359  idrespermg  19377  pmtrsn  19485  psgnsn  19486  abl1  19832  dprdz  19998  dprdsn  20004  simpgnsgd  20068  2nsgsimpgd  20070  ring1  20282  rng1nnzr  20747  pwssplit3  21051  lpival  21317  cnfldex  21350  pzriprnglem13  21468  pzriprnglem14  21469  frlmip  21753  islindf4  21813  evlsvvval  22069  evlssca  22070  evlsevl  22108  psdmul  22154  evls1sca  22309  mattposvs  22438  mat1dimelbas  22454  mat1dimscm  22458  mat1dimmul  22459  mat1rhmval  22462  m1detdiag  22580  mdetrlin  22585  mdetrsca2  22587  mdetrlin2  22590  mdetunilem5  22599  smadiadetglem2  22655  basdif0  22936  ordtbas  23175  leordtval2  23195  conncompid  23414  ptbasfi  23564  dfac14lem  23600  dfac14  23601  ptrescn  23622  xkoptsub  23637  pt1hmeo  23789  xpstopnlem1  23792  ufileu  23902  filufint  23903  uffix  23904  uffixsn  23908  flimclslem  23967  ptcmplem1  24035  imasdsf1olem  24356  icccmplem1  24806  icccmplem2  24807  rrxip  25375  rrxsca  25381  ehl1eudis  25405  elply2  26179  plyss  26182  plyeq0lem  26193  taylfval  26342  sltssnb  27779  lesrec  27809  eqcuts3  27814  0lt1s  27822  sltsleft  27870  sltsright  27871  addsval  27972  addsuniflem  28011  negsid  28051  negsunif  28065  mulsval  28119  sltmuls1  28157  sltmuls2  28158  precsexlem1  28217  precsexlem2  28218  precsexlem11  28227  n0fincut  28365  axlowdimlem15  29043  axlowdim  29048  snstriedgval  29125  vtxvalsnop  29128  iedgvalsnop  29129  upgr1eop  29202  upgr1eopALT  29204  uspgr1eop  29334  usgr1eop  29337  1loopgrvd2  29590  1loopgrvd0  29591  p1evtxdeqlem  29599  p1evtxdeq  29600  p1evtxdp1  29601  uspgrloopvtx  29602  uspgrloopiedg  29604  uspgrloopedg  29605  wlkp1lem4  29761  0pthonv  30217  eupth2lem3  30324  wlkl0  30455  0ofval  30876  suppovss  32773  padct  32810  resf1o  32822  elrgspnlem4  33326  elrspunsn  33512  drngidlhash  33517  0mplrim  33698  selvply1rhmlema  33702  selvply1rhmlemb  33703  selvply1rhmlem1  33704  selvply1rhmlem2  33705  selvply1rhmlem4  33707  zar0ring  34062  ordtconnlem1  34108  esumpr  34250  esumrnmpt2  34252  esumfzf  34253  prsiga  34315  rossros  34364  cntnevol  34412  omsmeas  34507  ccatmulgnn0dir  34726  ofcs1  34728  actfunsnf1o  34788  actfunsnrndisj  34789  reprsuc  34799  breprexplema  34814  bnj918  34949  bnj95  35046  bnj1489  35238  fineqvac  35297  subfacp1lem5  35412  erdszelem5  35423  erdszelem8  35426  cvmliftlem4  35516  cvmliftlem5  35517  cvmlift2lem6  35536  cvmlift2lem9  35539  cvmlift2lem12  35542  satfv1lem  35590  prv1n  35659  brapply  36164  lemsuccf  36167  altopthsn  36189  hfsn  36407  neibastop2lem  36588  topjoin  36593  onpsstopbas  36658  weiunse  36696  ttcsnexg  36748  bj-2uplex  37375  bj-restsn  37440  finixpnum  37972  ptrest  37986  poimirlem3  37990  poimirlem4  37991  poimirlem28  38015  fdc  38112  heiborlem8  38185  ismrer1  38205  grposnOLD  38249  zrdivrng  38320  lsatset  39482  ldualset  39617  lineset  40230  dvaset  41497  dvhset  41573  dibval  41634  dibfna  41646  sticksstones9  42639  frlmsnic  43026  elrfi  43143  wopprc  43475  dfac11  43507  kelac2  43510  safesnsupfidom1o  43861  sn1dom  43970  pr2dom  43971  tr3dom  43972  fvilbdRP  44134  brtrclfv2  44171  frege110  44417  frege133  44440  k0004lem3  44593  mnuprdlem1  44716  mnuprdlem2  44717  mnuprdlem3  44718  snelpwrVD  45274  nregmodelf1o  45459  fnchoice  45477  elmapsnd  45650  difmapsn  45657  unirnmapsn  45659  ssmapsn  45661  limcresiooub  46085  limcresioolb  46086  cnfdmsn  46325  dvsinax  46356  fourierdlem48  46597  fourierdlem49  46598  sge0sn  46822  sge0p1  46857  hoicvr  46991  ovnovollem1  47099  ovnovollem2  47100  vonvolmbllem  47103  nthrucw  47331  fsetsnf  47514  fsetsnf1  47515  fsetsnfo  47516  cfsetsnfsetfo  47523  setsv  47853  nnsum3primesprm  48281  mapsnop  48835  lindsrng01  48959  snlindsntorlem  48961  snlindsntor  48962  lmod1lem1  48978  lmod1lem2  48979  lmod1lem3  48980  lmod1lem4  48981  lmod1lem5  48982  lmod1  48983  lmod1zr  48984  fv1arycl  49128  1arympt1fv  49130  1arymaptfo  49134  eufsn2  49333  discsubclem  49553  discsubc  49554  iinfconstbas  49556  diag1f1lem  49796  setcsnterm  49980  setc1ocofval  49984  isinito2lem  49988  idfudiag1  50015  diag1f1olem  50023  prstchomval  50049  mndtcbasval  50070  mndtchom  50074  mndtcco  50075  incat  50091  setc1onsubc  50092  aacllem  50291