Theorem snex 5385

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

Assertion

Ref	Expression
snex	⊢ {𝐴} ∈ V

Proof of Theorem snex

Step	Hyp	Ref	Expression
1		dfsn2 4595	. 2 ⊢ {𝐴} = {𝐴, 𝐴}
2		prex 5384	. 2 ⊢ {𝐴, 𝐴} ∈ V
3	1, 2	eqeltri 2833	1 ⊢ {𝐴} ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3442  {csn 4582  {cpr 4584

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  ax-sep 5243  ax-pr 5379

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

This theorem is referenced by:  snexg  5386  elopg  5422  opi1  5424  op1stb  5427  opnz  5429  opeqsng  5459  opeqpr  5461  snopeqop  5462  opthwiener  5470  uniop  5471  0sn0ep  5536  frirr  5608  opthprc  5696  frsn  5720  relop  5807  snsn0non  6451  onnev  6453  funsneqopb  7107  fsnex  7239  tpex  7701  difsnexi  7716  sucexb  7759  elxp4  7874  elxp5  7875  fvclex  7913  1stval  7945  2ndval  7946  fnse  8085  suppsnop  8130  brtpos2  8184  frrlem13  8250  tfrlem12  8330  tfrlem16  8334  1oex  8417  naddunif  8631  mapsnd  8836  fvdiagfn  8841  mapsnconst  8842  mapsncnv  8843  mapsnf1o2  8844  ralxpmap  8846  elixpsn  8887  ixpsnf1o  8888  mapsnf1o  8889  ensn1  8970  2dom  8979  mapsnend  8985  snmapen  8987  en2sn  8990  xpsnen  9001  endisj  9004  xpsnen2g  9010  domunsncan  9017  enfixsn  9026  disjenex  9075  domssex2  9077  domssex  9078  map2xp  9087  pssnn  9105  snnen2o  9157  isinf  9177  ac6sfi  9196  fodomfiOLD  9242  fczfsuppd  9301  snopfsupp  9306  fisn  9342  tc2  9661  tcsni  9662  ranksuc  9789  djuex  9832  fseqenlem1  9946  djuassen  10101  mapdjuen  10103  djudom1  10105  djuinf  10111  ackbij1lem5  10145  cfsuc  10179  dcomex  10369  axdc3lem4  10375  axdc4lem  10377  ttukeylem3  10433  brdom7disj  10453  brdom6disj  10454  fpwwe2lem12  10565  nn0ex  12419  hashxplem  14368  hashf1lem1  14390  hashge3el3dif  14422  ofs1  14905  climconst2  15483  ramub1lem2  16967  cshwsex  17040  setsvalg  17105  setsid  17146  pwsbas  17419  pwsle  17425  pwssca  17429  pwssnf1o  17431  imasplusg  17450  imasmulr  17451  imasvsca  17453  imasip  17454  acsfn  17594  homaval  17967  funcsetcestrclem1  18089  mgm1  18595  sgrp1  18666  mnd1  18716  mnd1id  18717  efmnd1bas  18830  idresefmnd  18836  smndex1bas  18843  smndex1sgrp  18845  smndex1mnd  18847  smndex1id  18848  grp1  18989  grp1inv  18990  mulgfval  19011  triv1nsgd  19114  1nsgtrivd  19115  symg2bas  19334  idrespermg  19352  pmtrsn  19460  psgnsn  19461  abl1  19807  dprdz  19973  dprdsn  19979  simpgnsgd  20043  2nsgsimpgd  20045  ring1  20257  rng1nnzr  20720  pwssplit3  21025  cnfldex  21324  pzriprnglem13  21460  pzriprnglem14  21461  frlmip  21745  islindf4  21805  evlsvvval  22060  evlssca  22061  psdmul  22121  evls1sca  22279  mattposvs  22411  mat1dimelbas  22427  mat1dimscm  22431  mat1dimmul  22432  mat1rhmval  22435  m1detdiag  22553  mdetrlin  22558  mdetrsca2  22560  mdetrlin2  22563  mdetunilem5  22572  smadiadetglem2  22628  basdif0  22909  ordtbas  23148  leordtval2  23168  conncompid  23387  ptbasfi  23537  dfac14lem  23573  dfac14  23574  ptrescn  23595  xkoptsub  23610  pt1hmeo  23762  xpstopnlem1  23765  ufileu  23875  filufint  23876  uffix  23877  uffixsn  23881  flimclslem  23940  ptcmplem1  24008  imasdsf1olem  24329  icccmplem1  24779  icccmplem2  24780  rrxip  25358  rrxsca  25364  ehl1eudis  25388  elply2  26169  plyss  26172  plyeq0lem  26183  taylfval  26334  sltssnb  27777  lesrec  27807  eqcuts3  27812  0lt1s  27820  sltsleft  27868  sltsright  27869  addsval  27970  addsuniflem  28009  negsid  28049  negsunif  28063  mulsval  28117  sltmuls1  28155  sltmuls2  28156  precsexlem1  28215  precsexlem2  28216  precsexlem11  28225  n0fincut  28363  axlowdimlem15  29041  axlowdim  29046  snstriedgval  29123  vtxvalsnop  29126  iedgvalsnop  29127  upgr1eop  29200  upgr1eopALT  29202  uspgr1eop  29332  usgr1eop  29335  1loopgrvd2  29589  1loopgrvd0  29590  p1evtxdeqlem  29598  p1evtxdeq  29599  p1evtxdp1  29600  uspgrloopvtx  29601  uspgrloopiedg  29603  uspgrloopedg  29604  wlkp1lem4  29760  0pthonv  30216  eupth2lem3  30323  wlkl0  30454  0ofval  30875  suppovss  32771  resf1o  32820  elrgspnlem4  33339  elrspunsn  33522  drngidlhash  33527  zar0ring  34056  ordtconnlem1  34102  esumpr  34244  esumrnmpt2  34246  esumfzf  34247  prsiga  34309  rossros  34358  cntnevol  34406  omsmeas  34501  ccatmulgnn0dir  34720  ofcs1  34722  actfunsnf1o  34782  actfunsnrndisj  34783  reprsuc  34793  breprexplema  34808  bnj918  34943  bnj95  35040  bnj1489  35232  fineqvac  35294  subfacp1lem5  35400  erdszelem5  35411  erdszelem8  35414  cvmliftlem4  35504  cvmliftlem5  35505  cvmlift2lem6  35524  cvmlift2lem9  35527  cvmlift2lem12  35530  satfv1lem  35578  prv1n  35647  brapply  36152  lemsuccf  36155  altopthsn  36177  hfsn  36395  neibastop2lem  36576  topjoin  36581  onpsstopbas  36646  weiunse  36684  bj-2uplex  37270  bj-restsn  37335  finixpnum  37856  ptrest  37870  poimirlem3  37874  poimirlem4  37875  poimirlem28  37899  fdc  37996  heiborlem8  38069  ismrer1  38089  grposnOLD  38133  zrdivrng  38204  ldualset  39501  lineset  40114  dvaset  41381  dvhset  41457  dibval  41518  dibfna  41530  sticksstones9  42524  frlmsnic  42910  evlsevl  42932  elrfi  43051  wopprc  43387  dfac11  43419  kelac2  43422  safesnsupfidom1o  43773  sn1dom  43882  pr2dom  43883  tr3dom  43884  fvilbdRP  44046  brtrclfv2  44083  frege110  44329  frege133  44352  k0004lem3  44505  mnuprdlem1  44628  mnuprdlem2  44629  snelpwrVD  45186  nregmodelf1o  45371  fnchoice  45389  elmapsnd  45562  difmapsn  45570  unirnmapsn  45572  ssmapsn  45574  limcresiooub  46000  limcresioolb  46001  cnfdmsn  46240  dvsinax  46271  fourierdlem48  46512  fourierdlem49  46513  sge0sn  46737  sge0p1  46772  ovnovollem1  47014  ovnovollem2  47015  vonvolmbllem  47018  nthrucw  47244  fsetsnf  47411  fsetsnf1  47412  fsetsnfo  47413  cfsetsnfsetfo  47420  setsv  47738  nnsum3primesprm  48150  mapsnop  48704  lindsrng01  48828  snlindsntorlem  48830  snlindsntor  48831  lmod1lem1  48847  lmod1lem2  48848  lmod1lem3  48849  lmod1lem4  48850  lmod1lem5  48851  lmod1  48852  lmod1zr  48853  fv1arycl  48997  1arympt1fv  48999  1arymaptfo  49003  eufsn2  49202  discsubclem  49422  discsubc  49423  iinfconstbas  49425  diag1f1lem  49665  setcsnterm  49849  setc1ocofval  49853  isinito2lem  49857  idfudiag1  49884  diag1f1olem  49892  prstchomval  49918  mndtcbasval  49939  mndtchom  49943  mndtcco  49944  incat  49960  setc1onsubc  49961  aacllem  50160