Theorem snex 5411

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation and Pairing. See also snexALT 5355. (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 4607	. 2 ⊢ {𝐴} = {𝐴, 𝐴}
2		prex 5410	. 2 ⊢ {𝐴, 𝐴} ∈ V
3	1, 2	eqeltri 2865	1 ⊢ {𝐴} ∈ V

Syntax hints:   ∈ wcel 2149  Vcvv 3463  {csn 4594  {cpr 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-sn 4595  df-pr 4597

This theorem is referenced by:  snexg  5412  elopg  5449  opi1  5451  op1stb  5454  opnz  5456  opeqsng  5487  opeqpr  5489  snopeqop  5490  opthwiener  5498  uniop  5499  0sn0ep  5566  frirr  5638  opthprc  5726  frsn  5750  relop  5837  snsn0non  6488  onnev  6490  funsneqopb  7150  fsnex  7282  tpex  7744  difsnexi  7759  sucexb  7802  elxp4  7918  elxp5  7919  fvclex  7955  1stval  7987  2ndval  7988  fnse  8128  suppsnop  8173  brtpos2  8227  frrlem13  8294  tfrlem12  8375  tfrlem16  8379  1oex  8462  naddunif  8679  mapsnd  8883  fvdiagfn  8888  mapsnconst  8889  mapsncnv  8890  mapsnf1o2  8891  ralxpmap  8893  elixpsn  8934  ixpsnf1o  8935  mapsnf1o  8936  ensn1  9017  2dom  9026  mapsnend  9032  snmapen  9034  en2sn  9037  xpsnen  9048  endisj  9051  xpsnen2g  9057  domunsncan  9064  enfixsn  9073  disjenex  9122  domssex2  9124  domssex  9125  map2xp  9134  pssnn  9152  snnen2o  9204  isinf  9224  ac6sfi  9243  fczfsuppd  9345  snopfsupp  9350  fisn  9386  tc2  9708  tcsni  9709  ranksuc  9836  djuex  9893  fseqenlem1  10007  djuassen  10161  mapdjuen  10163  djudom1  10165  djuinf  10171  ackbij1lem5  10205  cfsuc  10240  dcomex  10430  axdc3lem4  10436  axdc4lem  10438  ttukeylem3  10494  brdom7disj  10514  brdom6disj  10515  fpwwe2lem12  10626  nn0ex  12509  hashxplem  14469  hashf1lem1  14491  hashge3el3dif  14523  ofs1  15006  climconst2  15598  ramub1lem2  17086  cshwsex  17159  setsvalg  17225  setsid  17266  pwsbas  17539  pwsle  17545  pwssca  17549  pwssnf1o  17551  imasplusg  17570  imasmulr  17571  imasvsca  17573  imasip  17574  acsfn  17714  homaval  18087  funcsetcestrclem1  18209  mgm1  18715  sgrp1  18786  mnd1  18836  mnd1id  18837  efmnd1bas  18951  idresefmnd  18957  smndex1gbas  18960  smndex1gid  18962  smndex1igid  18964  smndex1bas  18967  smndex1sgrp  18969  smndex1mnd  18971  smndex1id  18972  grp1  19112  grp1inv  19113  mulgfval  19134  triv1nsgd  19238  1nsgtrivd  19239  symg2bas  19462  idrespermg  19480  pmtrsn  19588  psgnsn  19589  abl1  19935  dprdz  20101  dprdsn  20107  simpgnsgd  20171  2nsgsimpgd  20173  ring1  20392  rng1nnzr  20856  pwssplit3  21159  lpival  21460  cnfldex  21493  pzriprnglem13  21611  pzriprnglem14  21612  frlmip  21896  islindf4  21956  evlsvvval  22212  evlssca  22213  evlsevl  22251  psdmul  22297  evls1sca  22451  mattposvs  22580  mat1dimelbas  22596  mat1dimscm  22600  mat1dimmul  22601  mat1rhmval  22604  m1detdiag  22722  mdetrlin  22727  mdetrsca2  22729  mdetrlin2  22732  mdetunilem5  22741  smadiadetglem2  22797  basdif0  23078  ordtbas  23317  leordtval2  23337  conncompid  23556  ptbasfi  23706  dfac14lem  23742  dfac14  23743  ptrescn  23764  xkoptsub  23779  pt1hmeo  23931  xpstopnlem1  23934  ufileu  24044  filufint  24045  uffix  24046  uffixsn  24050  flimclslem  24109  ptcmplem1  24177  imasdsf1olem  24498  icccmplem1  24948  icccmplem2  24949  rrxip  25517  rrxsca  25523  ehl1eudis  25547  elply2  26321  plyss  26324  plyeq0lem  26335  taylfval  26487  sltssnb  27927  lesrec  27957  eqcuts3  27962  0lt1s  27970  sltsleft  28018  sltsright  28019  addsval  28120  addsuniflem  28159  negsid  28199  negsunif  28213  mulsval  28267  sltmuls1  28305  sltmuls2  28306  precsexlem1  28365  precsexlem2  28366  precsexlem11  28375  n0fincut  28513  axlowdimlem15  29246  axlowdim  29251  snstriedgval  29328  vtxvalsnop  29331  iedgvalsnop  29332  upgr1eop  29405  upgr1eopALT  29407  uspgr1eop  29537  usgr1eop  29540  1loopgrvd2  29793  1loopgrvd0  29794  p1evtxdeqlem  29802  p1evtxdeq  29803  p1evtxdp1  29804  uspgrloopvtx  29805  uspgrloopiedg  29807  uspgrloopedg  29808  wlkp1lem4  29964  0pthonv  30420  eupth2lem3  30527  wlkl0  30658  0ofval  31079  suppovss  32966  padct  33003  resf1o  33015  elrgspnlem4  33505  elrspunsn  33680  drngidlhash  33685  fldlring  33733  0mplrim  33848  selvply1rhmlema  33852  selvply1rhmlemb  33853  selvply1rhmlem1  33854  selvply1rhmlem2  33855  selvply1rhmlem4  33857  zar0ring  34212  ordtconnlem1  34258  esumpr  34400  esumrnmpt2  34402  esumfzf  34403  prsiga  34465  rossros  34514  cntnevol  34562  omsmeas  34657  ccatmulgnn0dir  34876  ofcs1  34878  actfunsnf1o  34935  actfunsnrndisj  34936  reprsuc  34946  breprexplema  34961  bnj918  35099  bnj95  35196  bnj1489  35388  fineqvac  35451  subfacp1lem5  35574  erdszelem5  35585  erdszelem8  35588  cvmliftlem4  35678  cvmliftlem5  35679  cvmlift2lem6  35698  cvmlift2lem9  35701  cvmlift2lem12  35704  satfv1lem  35752  prv1n  35821  brapply  36326  lemsuccf  36329  altopthsn  36351  hfsn  36569  neibastop2lem  36759  topjoin  36764  onpsstopbas  36829  weiunse  36867  ttcsnexg  36919  bj-2uplex  37545  bj-restsn  37611  finixpnum  38143  ptrest  38157  poimirlem3  38161  poimirlem4  38162  poimirlem28  38186  fdc  38283  heiborlem8  38356  ismrer1  38376  grposnOLD  38420  zrdivrng  38491  lsatset  39653  ldualset  39788  lineset  40401  dvaset  41668  dvhset  41744  dibval  41805  dibfna  41817  sticksstones9  42810  frlmsnic  43199  elrfi  43316  wopprc  43648  dfac11  43680  kelac2  43683  safesnsupfidom1o  44034  sn1dom  44143  pr2dom  44144  tr3dom  44145  fvilbdRP  44307  brtrclfv2  44344  frege110  44590  frege133  44613  k0004lem3  44766  mnuprdlem1  44873  mnuprdlem2  44874  mnuprdlem3  44875  snelpwrVD  45430  nregmodelf1o  45615  fnchoice  45640  elmapsnd  45812  difmapsn  45819  unirnmapsn  45821  ssmapsn  45823  limcresiooub  46247  limcresioolb  46248  cnfdmsn  46487  dvsinax  46518  fourierdlem48  46759  fourierdlem49  46760  sge0sn  46984  sge0p1  47019  hoicvr  47153  ovnovollem1  47261  ovnovollem2  47262  vonvolmbllem  47265  nthrucw  47493  fsetsnf  47676  fsetsnf1  47677  fsetsnfo  47678  cfsetsnfsetfo  47685  setsv  48015  nnsum3primesprm  48443  mapsnop  49008  lindsrng01  49132  snlindsntorlem  49134  snlindsntor  49135  lmod1lem1  49151  lmod1lem2  49152  lmod1lem3  49153  lmod1lem4  49154  lmod1lem5  49155  lmod1  49156  lmod1zr  49157  fv1arycl  49301  1arympt1fv  49303  1arymaptfo  49307  eufsn2  49505  discsubclem  49725  discsubc  49726  iinfconstbas  49728  diag1f1lem  49968  setcsnterm  50152  setc1ocofval  50156  isinito2lem  50160  idfudiag1  50187  diag1f1olem  50195  prstchomval  50221  mndtcbasval  50242  mndtchom  50246  mndtcco  50247  incat  50263  setc1onsubc  50264  aacllem  50474