Theorem snex 5376

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

Assertion

Ref	Expression
snex	⊢ {𝐴} ∈ V

Proof of Theorem snex

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  {csn 4568  {cpr 4570

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 5231  ax-pr 5370

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 3432  df-un 3895  df-sn 4569  df-pr 4571

This theorem is referenced by:  snexg  5377  elopg  5414  opi1  5416  op1stb  5419  opnz  5421  opeqsng  5451  opeqpr  5453  snopeqop  5454  opthwiener  5462  uniop  5463  0sn0ep  5528  frirr  5600  opthprc  5688  frsn  5712  relop  5799  snsn0non  6443  onnev  6445  funsneqopb  7099  fsnex  7231  tpex  7693  difsnexi  7708  sucexb  7751  elxp4  7866  elxp5  7867  fvclex  7905  1stval  7937  2ndval  7938  fnse  8076  suppsnop  8121  brtpos2  8175  frrlem13  8241  tfrlem12  8321  tfrlem16  8325  1oex  8408  naddunif  8622  mapsnd  8827  fvdiagfn  8832  mapsnconst  8833  mapsncnv  8834  mapsnf1o2  8835  ralxpmap  8837  elixpsn  8878  ixpsnf1o  8879  mapsnf1o  8880  ensn1  8961  2dom  8970  mapsnend  8976  snmapen  8978  en2sn  8981  xpsnen  8992  endisj  8995  xpsnen2g  9001  domunsncan  9008  enfixsn  9017  disjenex  9066  domssex2  9068  domssex  9069  map2xp  9078  pssnn  9096  snnen2o  9148  isinf  9168  ac6sfi  9187  fodomfiOLD  9233  fczfsuppd  9292  snopfsupp  9297  fisn  9333  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  20743  pwssplit3  21048  lpival  21314  cnfldex  21347  pzriprnglem13  21483  pzriprnglem14  21484  frlmip  21768  islindf4  21828  evlsvvval  22081  evlssca  22082  psdmul  22142  evls1sca  22298  mattposvs  22430  mat1dimelbas  22446  mat1dimscm  22450  mat1dimmul  22451  mat1rhmval  22454  m1detdiag  22572  mdetrlin  22577  mdetrsca2  22579  mdetrlin2  22582  mdetunilem5  22591  smadiadetglem2  22647  basdif0  22928  ordtbas  23167  leordtval2  23187  conncompid  23406  ptbasfi  23556  dfac14lem  23592  dfac14  23593  ptrescn  23614  xkoptsub  23629  pt1hmeo  23781  xpstopnlem1  23784  ufileu  23894  filufint  23895  uffix  23896  uffixsn  23900  flimclslem  23959  ptcmplem1  24027  imasdsf1olem  24348  icccmplem1  24798  icccmplem2  24799  rrxip  25367  rrxsca  25373  ehl1eudis  25397  elply2  26171  plyss  26174  plyeq0lem  26185  taylfval  26335  sltssnb  27775  lesrec  27805  eqcuts3  27810  0lt1s  27818  sltsleft  27866  sltsright  27867  addsval  27968  addsuniflem  28007  negsid  28047  negsunif  28061  mulsval  28115  sltmuls1  28153  sltmuls2  28154  precsexlem1  28213  precsexlem2  28214  precsexlem11  28223  n0fincut  28361  axlowdimlem15  29039  axlowdim  29044  snstriedgval  29121  vtxvalsnop  29124  iedgvalsnop  29125  upgr1eop  29198  upgr1eopALT  29200  uspgr1eop  29330  usgr1eop  29333  1loopgrvd2  29587  1loopgrvd0  29588  p1evtxdeqlem  29596  p1evtxdeq  29597  p1evtxdp1  29598  uspgrloopvtx  29599  uspgrloopiedg  29601  uspgrloopedg  29602  wlkp1lem4  29758  0pthonv  30214  eupth2lem3  30321  wlkl0  30452  0ofval  30873  suppovss  32769  padct  32806  resf1o  32818  elrgspnlem4  33321  elrspunsn  33504  drngidlhash  33509  zar0ring  34038  ordtconnlem1  34084  esumpr  34226  esumrnmpt2  34228  esumfzf  34229  prsiga  34291  rossros  34340  cntnevol  34388  omsmeas  34483  ccatmulgnn0dir  34702  ofcs1  34704  actfunsnf1o  34764  actfunsnrndisj  34765  reprsuc  34775  breprexplema  34790  bnj918  34925  bnj95  35022  bnj1489  35214  fineqvac  35276  subfacp1lem5  35382  erdszelem5  35393  erdszelem8  35396  cvmliftlem4  35486  cvmliftlem5  35487  cvmlift2lem6  35506  cvmlift2lem9  35509  cvmlift2lem12  35512  satfv1lem  35560  prv1n  35629  brapply  36134  lemsuccf  36137  altopthsn  36159  hfsn  36377  neibastop2lem  36558  topjoin  36563  onpsstopbas  36628  weiunse  36666  ttcsnexg  36718  bj-2uplex  37345  bj-restsn  37410  finixpnum  37940  ptrest  37954  poimirlem3  37958  poimirlem4  37959  poimirlem28  37983  fdc  38080  heiborlem8  38153  ismrer1  38173  grposnOLD  38217  zrdivrng  38288  lsatset  39450  ldualset  39585  lineset  40198  dvaset  41465  dvhset  41541  dibval  41602  dibfna  41614  sticksstones9  42607  frlmsnic  42999  evlsevl  43021  elrfi  43140  wopprc  43476  dfac11  43508  kelac2  43511  safesnsupfidom1o  43862  sn1dom  43971  pr2dom  43972  tr3dom  43973  fvilbdRP  44135  brtrclfv2  44172  frege110  44418  frege133  44441  k0004lem3  44594  mnuprdlem1  44717  mnuprdlem2  44718  mnuprdlem3  44719  snelpwrVD  45275  nregmodelf1o  45460  fnchoice  45478  elmapsnd  45651  difmapsn  45659  unirnmapsn  45661  ssmapsn  45663  limcresiooub  46088  limcresioolb  46089  cnfdmsn  46328  dvsinax  46359  fourierdlem48  46600  fourierdlem49  46601  sge0sn  46825  sge0p1  46860  hoicvr  46994  ovnovollem1  47102  ovnovollem2  47103  vonvolmbllem  47106  nthrucw  47332  fsetsnf  47511  fsetsnf1  47512  fsetsnfo  47513  cfsetsnfsetfo  47520  setsv  47850  nnsum3primesprm  48278  mapsnop  48832  lindsrng01  48956  snlindsntorlem  48958  snlindsntor  48959  lmod1lem1  48975  lmod1lem2  48976  lmod1lem3  48977  lmod1lem4  48978  lmod1lem5  48979  lmod1  48980  lmod1zr  48981  fv1arycl  49125  1arympt1fv  49127  1arymaptfo  49131  eufsn2  49330  discsubclem  49550  discsubc  49551  iinfconstbas  49553  diag1f1lem  49793  setcsnterm  49977  setc1ocofval  49981  isinito2lem  49985  idfudiag1  50012  diag1f1olem  50020  prstchomval  50046  mndtcbasval  50067  mndtchom  50071  mndtcco  50072  incat  50088  setc1onsubc  50089  aacllem  50288