Theorem snex 5412

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

Assertion

Ref	Expression
snex	⊢ {𝐴} ∈ V

Proof of Theorem snex

Step	Hyp	Ref	Expression
1		dfsn2 4604	. 2 ⊢ {𝐴} = {𝐴, 𝐴}
2		prex 5411	. 2 ⊢ {𝐴, 𝐴} ∈ V
3	1, 2	eqeltri 2861	1 ⊢ {𝐴} ∈ V

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457  {csn 4591  {cpr 4593

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-sn 4592  df-pr 4594

This theorem is used by:  snexg  5413  elopg  5450  opi1  5452  op1stb  5455  opnz  5457  opeqsng  5488  opeqpr  5490  snopeqop  5491  opthwiener  5499  uniop  5500  0sn0ep  5567  frirr  5639  opthprc  5727  frsn  5751  relop  5838  snsn0non  6491  onnev  6493  funsneqopb  7155  fsnex  7290  tpex  7753  difsnexi  7766  sucexb  7809  elxp4  7925  elxp5  7926  fvclex  7962  1stval  7994  2ndval  7995  fnse  8135  suppsnop  8180  brtpos2  8234  frrlem13  8301  tfrlem12  8382  tfrlem16  8386  1oex  8469  naddunif  8686  mapsnd  8890  fvdiagfn  8895  mapsnconst  8896  mapsncnv  8897  mapsnf1o2  8898  ralxpmap  8900  elixpsn  8941  ixpsnf1o  8942  mapsnf1o  8943  ensn1  9024  2dom  9034  mapsnend  9040  snmapen  9042  en2sn  9045  xpsnen  9056  endisj  9059  xpsnen2g  9065  domunsncan  9072  enfixsn  9081  disjenex  9130  domssex2  9132  domssex  9133  map2xp  9142  pssnn  9160  snnen2o  9212  isinf  9232  ac6sfi  9251  fczfsuppd  9353  snopfsupp  9358  fisn  9394  tc2  9716  tcsni  9717  ranksuc  9844  djuex  9910  fseqenlem1  10024  djuassen  10178  mapdjuen  10180  djudom1  10182  djuinf  10188  ackbij1lem5  10222  cfsuc  10256  dcomex  10446  axdc3lem4  10452  axdc4lem  10454  ttukeylem3  10510  brdom7disj  10530  brdom6disj  10531  fpwwe2lem12  10642  nn0ex  12525  hashxplem  14488  hashf1lem1  14510  hashge3el3dif  14542  ofs1  15031  climconst2  15623  ramub1lem2  17109  cshwsex  17182  setsvalg  17248  setsid  17289  pwsbas  17562  pwsle  17568  pwssca  17572  pwssnf1o  17574  imasplusg  17593  imasmulr  17594  imasvsca  17596  imasip  17597  acsfn  17737  homaval  18110  funcsetcestrclem1  18232  mgm1  18740  sgrp1  18819  mnd1  18874  mnd1id  18875  efmnd1bas  18989  idresefmnd  18995  smndex1gbas  18998  smndex1gid  19000  smndex1igid  19002  smndex1bas  19005  smndex1sgrp  19007  smndex1mnd  19009  smndex1id  19010  grp1  19157  grp1inv  19158  mulgfval  19179  triv1nsgd  19283  1nsgtrivd  19284  symg2bas  19507  idrespermg  19525  pmtrsn  19633  psgnsn  19634  abl1  19980  dprdz  20146  dprdsn  20152  simpgnsgd  20216  2nsgsimpgd  20218  ring1  20439  rng1nnzr  20929  pwssplit3  21232  lpival  21542  cnfldex  21575  pzriprnglem13  21693  pzriprnglem14  21694  frlmip  21978  islindf4  22038  evlsvvval  22294  evlssca  22295  evlsevl  22333  psdmul  22379  evls1sca  22533  mattposvs  22662  mat1dimelbas  22678  mat1dimscm  22682  mat1dimmul  22683  mat1rhmval  22686  m1detdiag  22804  mdetrlin  22809  mdetrsca2  22811  mdetrlin2  22814  mdetunilem5  22823  smadiadetglem2  22879  basdif0  23160  ordtbas  23399  leordtval2  23419  conncompid  23638  ptbasfi  23789  dfac14lem  23825  dfac14  23826  ptrescn  23847  xkoptsub  23862  pt1hmeo  24014  xpstopnlem1  24017  ufileu  24127  filufint  24128  uffix  24129  uffixsn  24133  flimclslem  24192  ptcmplem1  24260  imasdsf1olem  24581  icccmplem1  25031  icccmplem2  25032  rrxip  25600  rrxsca  25606  ehl1eudis  25630  elply2  26404  plyss  26407  plyeq0lem  26418  taylfval  26573  sltssnb  28013  lesrec  28043  eqcuts3  28048  0lt1s  28056  sltsleft  28104  sltsright  28105  addsval  28206  addsuniflem  28245  negsid  28285  negsunif  28299  mulsval  28353  sltmuls1  28391  sltmuls2  28392  precsexlem1  28451  precsexlem2  28452  precsexlem11  28461  n0fincut  28599  axlowdimlem15  29361  axlowdim  29366  snstriedgval  29443  vtxvalsnop  29446  iedgvalsnop  29447  upgr1eop  29520  upgr1eopALT  29522  uspgr1eop  29655  usgr1eop  29658  1loopgrvd2  29911  1loopgrvd0  29912  p1evtxdeqlem  29920  p1evtxdeq  29921  p1evtxdp1  29922  uspgrloopvtx  29923  uspgrloopiedg  29925  uspgrloopedg  29926  wlkp1lem4  30082  0pthonv  30547  eupth2lem3  30658  wlkl0  30789  0ofval  31210  suppovss  33097  padct  33133  resf1o  33145  elrgspnlem4  33629  elrspunsn  33801  drngidlhash  33805  fldlring  33853  0mplrim  33968  selvply1rhmlema  33972  selvply1rhmlemb  33973  selvply1rhmlem1  33974  selvply1rhmlem2  33975  selvply1rhmlem4  33977  zar0ring  34332  ordtconnlem1  34378  esumpr  34520  esumrnmpt2  34522  esumfzf  34523  prsiga  34585  rossros  34635  cntnevol  34683  omsmeas  34778  ccatmulgnn0dir  34997  ofcs1  34999  actfunsnf1o  35056  actfunsnrndisj  35057  reprsuc  35067  breprexplema  35082  bnj918  35220  bnj95  35317  bnj1489  35509  fineqvac  35586  kard0  35624  kardsn  35630  subfacp1lem5  35713  erdszelem5  35724  erdszelem8  35727  cvmliftlem4  35817  cvmliftlem5  35818  cvmlift2lem6  35837  cvmlift2lem9  35840  cvmlift2lem12  35843  satfv1lem  35891  prv1n  35960  brapply  36465  lemsuccf  36468  altopthsn  36490  hfsn  36708  neibastop2lem  36928  topjoin  36933  onpsstopbas  36998  weiunse  37036  ttcsnexg  37088  bj-2uplex  37715  bj-restsn  37781  finixpnum  38313  ptrest  38327  poimirlem3  38331  poimirlem4  38332  poimirlem28  38356  fdc  38454  heiborlem8  38527  ismrer1  38547  grposnOLD  38591  zrdivrng  38662  lsatset  39822  ldualset  39957  lineset  40570  dvaset  41837  dvhset  41913  dibval  41974  dibfna  41986  sticksstones9  42979  frlmsnic  43366  elrfi  43483  wopprc  43815  dfac11  43847  kelac2  43850  safesnsupfidom1o  44201  sn1dom  44310  pr2dom  44311  tr3dom  44312  fvilbdRP  44474  brtrclfv2  44511  frege110  44757  frege133  44780  k0004lem3  44933  mnuprdlem1  45040  mnuprdlem2  45041  mnuprdlem3  45042  snelpwrVD  45597  nregmodelf1o  45782  fnchoice  45807  elmapsnd  45979  difmapsn  45986  unirnmapsn  45988  ssmapsn  45990  limcresiooub  46414  limcresioolb  46415  cnfdmsn  46654  dvsinax  46685  fourierdlem48  46926  fourierdlem49  46927  sge0sn  47151  sge0p1  47186  hoicvr  47320  ovnovollem1  47428  ovnovollem2  47429  vonvolmbllem  47432  nthrucw  47665  fsetsnf  47846  fsetsnf1  47847  fsetsnfo  47848  cfsetsnfsetfo  47855  setsv  48185  nnsum3primesprm  48613  mapsnop  49181  lindsrng01  49305  snlindsntorlem  49307  snlindsntor  49308  lmod1lem1  49324  lmod1lem2  49325  lmod1lem3  49326  lmod1lem4  49327  lmod1lem5  49328  lmod1  49329  lmod1zr  49330  fv1arycl  49474  1arympt1fv  49476  1arymaptfo  49480  eufsn2  49678  discsubclem  49898  discsubc  49899  iinfconstbas  49901  diag1f1lem  50141  setcsnterm  50325  setc1ocofval  50329  isinito2lem  50333  idfudiag1  50360  diag1f1olem  50368  prstchomval  50394  mndtcbasval  50415  mndtchom  50419  mndtcco  50420  incat  50436  setc1onsubc  50437  aacllem  50678