Theorem snex 5374

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation and Pairing. See also snexALT 5318. (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 5373	. 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 5368

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  5375  elopg  5412  opi1  5414  op1stb  5417  opnz  5419  opeqsng  5449  opeqpr  5451  snopeqop  5452  opthwiener  5460  uniop  5461  0sn0ep  5526  frirr  5598  opthprc  5686  frsn  5710  relop  5797  snsn0non  6441  onnev  6443  funsneqopb  7097  fsnex  7229  tpex  7691  difsnexi  7706  sucexb  7749  elxp4  7864  elxp5  7865  fvclex  7903  1stval  7935  2ndval  7936  fnse  8074  suppsnop  8119  brtpos2  8173  frrlem13  8239  tfrlem12  8319  tfrlem16  8323  1oex  8406  naddunif  8620  mapsnd  8825  fvdiagfn  8830  mapsnconst  8831  mapsncnv  8832  mapsnf1o2  8833  ralxpmap  8835  elixpsn  8876  ixpsnf1o  8877  mapsnf1o  8878  ensn1  8959  2dom  8968  mapsnend  8974  snmapen  8976  en2sn  8979  xpsnen  8990  endisj  8993  xpsnen2g  8999  domunsncan  9006  enfixsn  9015  disjenex  9064  domssex2  9066  domssex  9067  map2xp  9076  pssnn  9094  snnen2o  9146  isinf  9166  ac6sfi  9185  fodomfiOLD  9231  fczfsuppd  9290  snopfsupp  9295  fisn  9331  tc2  9650  tcsni  9651  ranksuc  9778  djuex  9821  fseqenlem1  9935  djuassen  10090  mapdjuen  10092  djudom1  10094  djuinf  10100  ackbij1lem5  10134  cfsuc  10168  dcomex  10358  axdc3lem4  10364  axdc4lem  10366  ttukeylem3  10422  brdom7disj  10442  brdom6disj  10443  fpwwe2lem12  10554  nn0ex  12408  hashxplem  14357  hashf1lem1  14379  hashge3el3dif  14411  ofs1  14894  climconst2  15472  ramub1lem2  16956  cshwsex  17029  setsvalg  17094  setsid  17135  pwsbas  17408  pwsle  17414  pwssca  17418  pwssnf1o  17420  imasplusg  17439  imasmulr  17440  imasvsca  17442  imasip  17443  acsfn  17583  homaval  17956  funcsetcestrclem1  18078  mgm1  18584  sgrp1  18655  mnd1  18705  mnd1id  18706  efmnd1bas  18819  idresefmnd  18825  smndex1gbas  18828  smndex1gid  18830  smndex1igid  18832  smndex1bas  18835  smndex1sgrp  18837  smndex1mnd  18839  smndex1id  18840  grp1  18981  grp1inv  18982  mulgfval  19003  triv1nsgd  19106  1nsgtrivd  19107  symg2bas  19326  idrespermg  19344  pmtrsn  19452  psgnsn  19453  abl1  19799  dprdz  19965  dprdsn  19971  simpgnsgd  20035  2nsgsimpgd  20037  ring1  20249  rng1nnzr  20710  pwssplit3  21015  lpival  21281  cnfldex  21314  pzriprnglem13  21450  pzriprnglem14  21451  frlmip  21735  islindf4  21795  evlsvvval  22049  evlssca  22050  psdmul  22110  evls1sca  22266  mattposvs  22398  mat1dimelbas  22414  mat1dimscm  22418  mat1dimmul  22419  mat1rhmval  22422  m1detdiag  22540  mdetrlin  22545  mdetrsca2  22547  mdetrlin2  22550  mdetunilem5  22559  smadiadetglem2  22615  basdif0  22896  ordtbas  23135  leordtval2  23155  conncompid  23374  ptbasfi  23524  dfac14lem  23560  dfac14  23561  ptrescn  23582  xkoptsub  23597  pt1hmeo  23749  xpstopnlem1  23752  ufileu  23862  filufint  23863  uffix  23864  uffixsn  23868  flimclslem  23927  ptcmplem1  23995  imasdsf1olem  24316  icccmplem1  24766  icccmplem2  24767  rrxip  25335  rrxsca  25341  ehl1eudis  25365  elply2  26142  plyss  26145  plyeq0lem  26156  taylfval  26306  sltssnb  27749  lesrec  27779  eqcuts3  27784  0lt1s  27792  sltsleft  27840  sltsright  27841  addsval  27942  addsuniflem  27981  negsid  28021  negsunif  28035  mulsval  28089  sltmuls1  28127  sltmuls2  28128  precsexlem1  28187  precsexlem2  28188  precsexlem11  28197  n0fincut  28335  axlowdimlem15  29013  axlowdim  29018  snstriedgval  29095  vtxvalsnop  29098  iedgvalsnop  29099  upgr1eop  29172  upgr1eopALT  29174  uspgr1eop  29304  usgr1eop  29307  1loopgrvd2  29561  1loopgrvd0  29562  p1evtxdeqlem  29570  p1evtxdeq  29571  p1evtxdp1  29572  uspgrloopvtx  29573  uspgrloopiedg  29575  uspgrloopedg  29576  wlkp1lem4  29732  0pthonv  30188  eupth2lem3  30295  wlkl0  30426  0ofval  30847  suppovss  32743  padct  32780  resf1o  32792  elrgspnlem4  33311  elrspunsn  33494  drngidlhash  33499  zar0ring  34028  ordtconnlem1  34074  esumpr  34216  esumrnmpt2  34218  esumfzf  34219  prsiga  34281  rossros  34330  cntnevol  34378  omsmeas  34473  ccatmulgnn0dir  34692  ofcs1  34694  actfunsnf1o  34754  actfunsnrndisj  34755  reprsuc  34765  breprexplema  34780  bnj918  34915  bnj95  35012  bnj1489  35204  fineqvac  35266  subfacp1lem5  35372  erdszelem5  35383  erdszelem8  35386  cvmliftlem4  35476  cvmliftlem5  35477  cvmlift2lem6  35496  cvmlift2lem9  35499  cvmlift2lem12  35502  satfv1lem  35550  prv1n  35619  brapply  36124  lemsuccf  36127  altopthsn  36149  hfsn  36367  neibastop2lem  36548  topjoin  36553  onpsstopbas  36618  weiunse  36656  ttcsnexg  36708  bj-2uplex  37327  bj-restsn  37392  finixpnum  37917  ptrest  37931  poimirlem3  37935  poimirlem4  37936  poimirlem28  37960  fdc  38057  heiborlem8  38130  ismrer1  38150  grposnOLD  38194  zrdivrng  38265  lsatset  39427  ldualset  39562  lineset  40175  dvaset  41442  dvhset  41518  dibval  41579  dibfna  41591  sticksstones9  42585  frlmsnic  42984  evlsevl  43006  elrfi  43125  wopprc  43461  dfac11  43493  kelac2  43496  safesnsupfidom1o  43847  sn1dom  43956  pr2dom  43957  tr3dom  43958  fvilbdRP  44120  brtrclfv2  44157  frege110  44403  frege133  44426  k0004lem3  44579  mnuprdlem1  44702  mnuprdlem2  44703  mnuprdlem3  44704  snelpwrVD  45260  nregmodelf1o  45445  fnchoice  45463  elmapsnd  45636  difmapsn  45644  unirnmapsn  45646  ssmapsn  45648  limcresiooub  46074  limcresioolb  46075  cnfdmsn  46314  dvsinax  46345  fourierdlem48  46586  fourierdlem49  46587  sge0sn  46811  sge0p1  46846  hoicvr  46980  ovnovollem1  47088  ovnovollem2  47089  vonvolmbllem  47092  nthrucw  47318  fsetsnf  47485  fsetsnf1  47486  fsetsnfo  47487  cfsetsnfsetfo  47494  setsv  47812  nnsum3primesprm  48224  mapsnop  48778  lindsrng01  48902  snlindsntorlem  48904  snlindsntor  48905  lmod1lem1  48921  lmod1lem2  48922  lmod1lem3  48923  lmod1lem4  48924  lmod1lem5  48925  lmod1  48926  lmod1zr  48927  fv1arycl  49071  1arympt1fv  49073  1arymaptfo  49077  eufsn2  49276  discsubclem  49496  discsubc  49497  iinfconstbas  49499  diag1f1lem  49739  setcsnterm  49923  setc1ocofval  49927  isinito2lem  49931  idfudiag1  49958  diag1f1olem  49966  prstchomval  49992  mndtcbasval  50013  mndtchom  50017  mndtcco  50018  incat  50034  setc1onsubc  50035  aacllem  50234