Theorem snex 5404

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

Assertion

Ref	Expression
snex	⊢ {𝐴} ∈ V

Proof of Theorem snex

Step	Hyp	Ref	Expression
1		dfsn2 4597	. 2 ⊢ {𝐴} = {𝐴, 𝐴}
2		prex 5403	. 2 ⊢ {𝐴, 𝐴} ∈ V
3	1, 2	eqeltri 2860	1 ⊢ {𝐴} ∈ V

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  {csn 4588  {cpr 4590

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  snexg  5405  elopg  5442  opi1  5444  op1stb  5447  opnz  5449  opeqsng  5482  opeqpr  5484  snopeqop  5485  opthwiener  5494  uniop  5495  0sn0ep  5562  frirr  5634  opthprc  5722  frsn  5747  relop  5838  snsn0non  6515  onnev  6517  funsneqopb  7188  fsnex  7322  tpex  7794  difsnexi  7807  sucexb  7852  elxp4  7968  elxp5  7969  fvclex  8005  1stval  8037  2ndval  8038  fnse  8187  suppsnop  8233  brtpos2  8287  frrlem13  8354  tfrlem12  8435  tfrlem16  8439  1oex  8524  naddunif  8741  mapsnd  8952  fvdiagfn  8957  mapsnconst  8958  mapsncnv  8959  mapsnf1o2  8960  ralxpmap  8962  elixpsn  9003  ixpsnf1o  9004  mapsnf1o  9005  ensn1  9086  2dom  9096  mapsnend  9102  snmapen  9104  en2sn  9107  xpsnen  9118  endisj  9121  xpsnen2g  9127  domunsncan  9134  enfixsn  9143  disjenex  9192  domssex2  9194  domssex  9195  map2xp  9204  pssnn  9222  snnen2o  9274  isinf  9294  ac6sfi  9313  fczfsuppd  9415  snopfsupp  9420  fisn  9456  tc2  9778  tcsni  9779  ranksuc  9919  hfsnOLD  9958  djuex  10026  fseqenlem1  10142  djuassen  10296  mapdjuen  10298  djudom1  10300  djuinf  10306  ackbij1lem5  10340  cfsuc  10374  dcomex  10564  axdc3lem4  10570  axdc4lem  10572  ttukeylem3  10628  brdom7disj  10649  brdom6disj  10650  fpwwe2lem12  10766  nn0ex  12652  hashxplem  14619  hashf1lem1  14641  hashge3el3dif  14673  ofs1  15166  climconst2  15759  ramub1lem2  17249  cshwsex  17322  setsvalg  17388  setsid  17429  pwsbas  17708  pwsle  17714  pwssca  17718  pwssnf1o  17720  imasplusg  17739  imasmulr  17740  imasvsca  17742  imasip  17743  acsfn  17883  homaval  18256  funcsetcestrclem1  18378  mgm1  18886  sgrp1  18968  mnd1  19023  mnd1id  19024  efmnd1bas  19139  idresefmnd  19145  smndex1gbas  19148  smndex1gid  19150  smndex1igid  19152  smndex1bas  19155  smndex1sgrp  19157  smndex1mnd  19159  smndex1id  19160  grp1  19307  grp1inv  19308  mulgfval  19329  triv1nsgd  19433  1nsgtrivd  19434  symg2bas  19658  idrespermg  19676  pmtrsn  19784  psgnsn  19785  abl1  20131  dprdz  20297  dprdsn  20303  simpgnsgd  20367  2nsgsimpgd  20369  ring1  20592  rng1nnzr  21084  pwssplit3  21387  lpival  21699  cnfldex  21732  pzriprnglem13  21854  pzriprnglem14  21855  frlmip  22139  islindf4  22199  evlsvvval  22457  evlssca  22458  evlsevl  22496  psdmul  22542  evls1sca  22696  mattposvs  22825  mat1dimelbas  22841  mat1dimscm  22845  mat1dimmul  22846  mat1rhmval  22849  m1detdiag  22967  mdetrlin  22972  mdetrsca2  22974  mdetrlin2  22977  mdetunilem5  22986  smadiadetglem2  23042  basdif0  23326  ordtbas  23565  leordtval2  23585  conncompid  23804  ptbasfi  23955  dfac14lem  23991  dfac14  23992  ptrescn  24013  xkoptsub  24028  pt1hmeo  24180  xpstopnlem1  24183  ufileu  24293  filufint  24294  uffix  24295  uffixsn  24299  flimclslem  24358  ptcmplem1  24426  imasdsf1olem  24747  icccmplem1  25197  icccmplem2  25198  rrxip  25766  rrxsca  25772  ehl1eudis  25796  elply2  26569  plyss  26572  plyeq0lem  26584  taylfval  26743  sltssnb  28212  lesrec  28242  eqcuts3  28247  0lt1s  28255  sltsleft  28303  sltsright  28304  addsval  28405  addsuniflem  28444  negsid  28484  negsunif  28498  mulsval  28552  sltmuls1  28590  sltmuls2  28591  precsexlem1  28650  precsexlem2  28651  precsexlem11  28660  n0fincut  28798  axlowdimlem15  29591  axlowdim  29596  snstriedgval  29673  vtxvalsnop  29676  iedgvalsnop  29677  upgr1eop  29750  upgr1eopALT  29752  uspgr1eop  29885  usgr1eop  29888  1loopgrvd2  30141  1loopgrvd0  30142  p1evtxdeqlem  30150  p1evtxdeq  30151  p1evtxdp1  30152  uspgrloopvtx  30153  uspgrloopiedg  30155  uspgrloopedg  30156  wlkp1lem4  30312  0pthonv  30777  eupth2lem3  30894  wlkl0  31025  0ofval  31446  suppovss  33371  padct  33407  resf1o  33418  elrgspnlem4  33905  elrspunsn  34083  drngidlhash  34087  fldlring  34135  0mplrim  34257  selvply1rhmlema  34261  selvply1rhmlemb  34262  selvply1rhmlem1  34263  selvply1rhmlem2  34264  selvply1rhmlem4  34266  zar0ring  34621  ordtconnlem1  34667  esumpr  34809  esumrnmpt2  34811  esumfzf  34812  prsiga  34874  rossros  34924  cntnevol  34972  omsmeas  35066  ccatmulgnn0dir  35285  ofcs1  35287  actfunsnf1o  35344  actfunsnrndisj  35345  reprsuc  35355  breprexplema  35370  bnj918  35508  bnj95  35605  bnj1489  35797  fineqvac  35925  kard0  35963  kardsn  35969  subfacp1lem5  36157  erdszelem5  36168  erdszelem8  36171  cvmliftlem4  36261  cvmliftlem5  36262  cvmlift2lem6  36281  cvmlift2lem9  36284  cvmlift2lem12  36287  satfv1lem  36335  prv1n  36404  brapply  36915  lemsuccf  36918  altopthsn  36941  neibastop2lem  37363  topjoin  37368  onpsstopbas  37433  weiunse  37471  ttcsnexg  37523  bj-2uplex  38150  bj-restsn  38273  finixpnum  38796  ptrest  38805  poimirlem3  38809  poimirlem4  38810  poimirlem28  38834  dfproplem  38909  fdc  38945  heiborlem8  39018  ismrer1  39038  grposnOLD  39082  zrdivrng  39153  lsatset  40313  ldualset  40448  lineset  41061  dvaset  42328  dvhset  42404  dibval  42465  dibfna  42477  sticksstones9  43470  frlmsnic  43870  elrfi  43971  wopprc  44303  dfac11  44330  kelac2  44333  safesnsupfidom1o  44679  sn1dom  44788  pr2dom  44789  tr3dom  44790  fvilbdRP  44951  brtrclfv2  44988  frege110  45234  frege133  45257  k0004lem3  45410  mnuprdlem1  45517  mnuprdlem2  45518  mnuprdlem3  45519  snelpwrVD  46073  nregmodelf1o  46269  fnchoice  46320  elmapsnd  46491  difmapsn  46498  unirnmapsn  46500  ssmapsn  46502  limcresiooub  46925  limcresioolb  46926  cnfdmsn  47165  dvsinax  47196  fourierdlem48  47437  fourierdlem49  47438  sge0sn  47662  sge0p1  47697  hoicvr  47831  ovnovollem1  47939  ovnovollem2  47940  vonvolmbllem  47943  numtowerdt  48189  fsetsnf  48394  fsetsnf1  48395  fsetsnfo  48396  cfsetsnfsetfo  48403  setsv  48733  nnsum3primesprm  49161  linply  49713  mapsnop  49787  lindsrng01  49911  snlindsntorlem  49913  snlindsntor  49914  lmod1lem1  49930  lmod1lem2  49931  lmod1lem3  49932  lmod1lem4  49933  lmod1lem5  49934  lmod1  49935  lmod1zr  49936  fv1arycl  50080  1arympt1fv  50082  1arymaptfo  50086  eufsn2  50285  discsubclem  50508  discsubc  50509  iinfconstbas  50511  diag1f1lem  50759  setcsnterm  50956  setc1ocofval  50960  isinito2lem  50964  idfudiag1  50991  diag1f1olem  50999  prstchomval  51028  mndtcbasval  51049  mndtchom  51053  mndtcco  51054  incat  51070  setc1onsubc  51071  parhomval  51074  parhomidval  51077  parcatid2  51094  parcatid  51095  parmapfunc2  51105  aacllem  51367