Theorem snex 5397

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation and Pairing. See also snexALT 5345. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) Avoid ax-nul 5260 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 5396	. 2 ⊢ {𝐴, 𝐴} ∈ V
3	1, 2	eqeltri 2857	1 ⊢ {𝐴} ∈ V

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  {csn 4584  {cpr 4586

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  snexg  5398  elopg  5435  opi1  5437  op1stb  5440  opnz  5442  opeqsng  5475  opeqpr  5477  snopeqop  5478  opthwiener  5487  uniop  5488  0sn0ep  5555  frirr  5627  opthprc  5715  frsn  5739  relop  5828  snsn0non  6488  onnev  6490  funsneqopb  7154  fsnex  7289  tpex  7760  difsnexi  7773  sucexb  7816  elxp4  7932  elxp5  7933  fvclex  7969  1stval  8001  2ndval  8002  fnse  8143  suppsnop  8188  brtpos2  8242  frrlem13  8309  tfrlem12  8390  tfrlem16  8394  1oex  8479  naddunif  8696  mapsnd  8907  fvdiagfn  8912  mapsnconst  8913  mapsncnv  8914  mapsnf1o2  8915  ralxpmap  8917  elixpsn  8958  ixpsnf1o  8959  mapsnf1o  8960  ensn1  9041  2dom  9051  mapsnend  9057  snmapen  9059  en2sn  9062  xpsnen  9073  endisj  9076  xpsnen2g  9082  domunsncan  9089  enfixsn  9098  disjenex  9147  domssex2  9149  domssex  9150  map2xp  9159  pssnn  9177  snnen2o  9229  isinf  9249  ac6sfi  9268  fczfsuppd  9371  snopfsupp  9376  fisn  9412  tc2  9734  tcsni  9735  ranksuc  9875  hfsnOLD  9914  djuex  9982  fseqenlem1  10096  djuassen  10250  mapdjuen  10252  djudom1  10254  djuinf  10260  ackbij1lem5  10294  cfsuc  10328  dcomex  10518  axdc3lem4  10524  axdc4lem  10526  ttukeylem3  10582  brdom7disj  10603  brdom6disj  10604  fpwwe2lem12  10720  nn0ex  12605  hashxplem  14571  hashf1lem1  14593  hashge3el3dif  14625  ofs1  15116  climconst2  15708  ramub1lem2  17198  cshwsex  17271  setsvalg  17337  setsid  17378  pwsbas  17651  pwsle  17657  pwssca  17661  pwssnf1o  17663  imasplusg  17682  imasmulr  17683  imasvsca  17685  imasip  17686  acsfn  17826  homaval  18199  funcsetcestrclem1  18321  mgm1  18829  sgrp1  18911  mnd1  18966  mnd1id  18967  efmnd1bas  19082  idresefmnd  19088  smndex1gbas  19091  smndex1gid  19093  smndex1igid  19095  smndex1bas  19098  smndex1sgrp  19100  smndex1mnd  19102  smndex1id  19103  grp1  19250  grp1inv  19251  mulgfval  19272  triv1nsgd  19376  1nsgtrivd  19377  symg2bas  19600  idrespermg  19618  pmtrsn  19726  psgnsn  19727  abl1  20073  dprdz  20239  dprdsn  20245  simpgnsgd  20309  2nsgsimpgd  20311  ring1  20534  rng1nnzr  21026  pwssplit3  21329  lpival  21641  cnfldex  21674  pzriprnglem13  21792  pzriprnglem14  21793  frlmip  22077  islindf4  22137  evlsvvval  22395  evlssca  22396  evlsevl  22434  psdmul  22480  evls1sca  22634  mattposvs  22763  mat1dimelbas  22779  mat1dimscm  22783  mat1dimmul  22784  mat1rhmval  22787  m1detdiag  22905  mdetrlin  22910  mdetrsca2  22912  mdetrlin2  22915  mdetunilem5  22924  smadiadetglem2  22980  basdif0  23264  ordtbas  23503  leordtval2  23523  conncompid  23742  ptbasfi  23893  dfac14lem  23929  dfac14  23930  ptrescn  23951  xkoptsub  23966  pt1hmeo  24118  xpstopnlem1  24121  ufileu  24231  filufint  24232  uffix  24233  uffixsn  24237  flimclslem  24296  ptcmplem1  24364  imasdsf1olem  24685  icccmplem1  25135  icccmplem2  25136  rrxip  25704  rrxsca  25710  ehl1eudis  25734  elply2  26507  plyss  26510  plyeq0lem  26522  taylfval  26679  sltssnb  28148  lesrec  28178  eqcuts3  28183  0lt1s  28191  sltsleft  28239  sltsright  28240  addsval  28341  addsuniflem  28380  negsid  28420  negsunif  28434  mulsval  28488  sltmuls1  28526  sltmuls2  28527  precsexlem1  28586  precsexlem2  28587  precsexlem11  28596  n0fincut  28734  axlowdimlem15  29527  axlowdim  29532  snstriedgval  29609  vtxvalsnop  29612  iedgvalsnop  29613  upgr1eop  29686  upgr1eopALT  29688  uspgr1eop  29821  usgr1eop  29824  1loopgrvd2  30077  1loopgrvd0  30078  p1evtxdeqlem  30086  p1evtxdeq  30087  p1evtxdp1  30088  uspgrloopvtx  30089  uspgrloopiedg  30091  uspgrloopedg  30092  wlkp1lem4  30248  0pthonv  30713  eupth2lem3  30830  wlkl0  30961  0ofval  31382  suppovss  33267  padct  33303  resf1o  33315  elrgspnlem4  33799  elrspunsn  33972  drngidlhash  33976  fldlring  34024  0mplrim  34139  selvply1rhmlema  34143  selvply1rhmlemb  34144  selvply1rhmlem1  34145  selvply1rhmlem2  34146  selvply1rhmlem4  34148  zar0ring  34503  ordtconnlem1  34549  esumpr  34691  esumrnmpt2  34693  esumfzf  34694  prsiga  34756  rossros  34806  cntnevol  34854  omsmeas  34948  ccatmulgnn0dir  35167  ofcs1  35169  actfunsnf1o  35226  actfunsnrndisj  35227  reprsuc  35237  breprexplema  35252  bnj918  35390  bnj95  35487  bnj1489  35679  fineqvac  35767  kard0  35805  kardsn  35811  subfacp1lem5  35928  erdszelem5  35939  erdszelem8  35942  cvmliftlem4  36032  cvmliftlem5  36033  cvmlift2lem6  36052  cvmlift2lem9  36055  cvmlift2lem12  36058  satfv1lem  36106  prv1n  36175  brapply  36680  lemsuccf  36683  altopthsn  36706  neibastop2lem  37128  topjoin  37133  onpsstopbas  37198  weiunse  37236  ttcsnexg  37288  bj-2uplex  37915  bj-restsn  37983  finixpnum  38508  ptrest  38517  poimirlem3  38521  poimirlem4  38522  poimirlem28  38546  dfproplem  38621  fdc  38659  heiborlem8  38732  ismrer1  38752  grposnOLD  38796  zrdivrng  38867  lsatset  40027  ldualset  40162  lineset  40775  dvaset  42042  dvhset  42118  dibval  42179  dibfna  42191  sticksstones9  43184  frlmsnic  43584  elrfi  43684  wopprc  44016  dfac11  44048  kelac2  44051  safesnsupfidom1o  44402  sn1dom  44511  pr2dom  44512  tr3dom  44513  fvilbdRP  44675  brtrclfv2  44712  frege110  44958  frege133  44981  k0004lem3  45134  mnuprdlem1  45241  mnuprdlem2  45242  mnuprdlem3  45243  snelpwrVD  45798  nregmodelf1o  45983  fnchoice  46015  elmapsnd  46187  difmapsn  46194  unirnmapsn  46196  ssmapsn  46198  limcresiooub  46621  limcresioolb  46622  cnfdmsn  46861  dvsinax  46892  fourierdlem48  47133  fourierdlem49  47134  sge0sn  47358  sge0p1  47393  hoicvr  47527  ovnovollem1  47635  ovnovollem2  47636  vonvolmbllem  47639  numtowerdt  47885  fsetsnf  48090  fsetsnf1  48091  fsetsnfo  48092  cfsetsnfsetfo  48099  setsv  48429  nnsum3primesprm  48857  mapsnop  49425  lindsrng01  49549  snlindsntorlem  49551  snlindsntor  49552  lmod1lem1  49568  lmod1lem2  49569  lmod1lem3  49570  lmod1lem4  49571  lmod1lem5  49572  lmod1  49573  lmod1zr  49574  fv1arycl  49718  1arympt1fv  49720  1arymaptfo  49724  eufsn2  49922  discsubclem  50140  discsubc  50141  iinfconstbas  50143  diag1f1lem  50383  setcsnterm  50567  setc1ocofval  50571  isinito2lem  50575  idfudiag1  50602  diag1f1olem  50610  prstchomval  50636  mndtcbasval  50657  mndtchom  50661  mndtcco  50662  incat  50678  setc1onsubc  50679  aacllem  50908