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 5259 and shorten proof. (Revised by GG, 6-Mar-2026.)

Assertion

Ref	Expression
snex	⊢ {𝐴} ∈ V

Proof of Theorem snex

Step	Hyp	Ref	Expression
1		dfsn2 4593	. 2 ⊢ {𝐴} = {𝐴, 𝐴}
2		prex 5396	. 2 ⊢ {𝐴, 𝐴} ∈ V
3	1, 2	eqeltri 2856	1 ⊢ {𝐴} ∈ V

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  {csn 4584  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4150  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  5740  relop  5829  snsn0non  6492  onnev  6494  funsneqopb  7161  fsnex  7295  tpex  7766  difsnexi  7779  sucexb  7822  elxp4  7938  elxp5  7939  fvclex  7975  1stval  8007  2ndval  8008  fnse  8157  suppsnop  8203  brtpos2  8257  frrlem13  8324  tfrlem12  8405  tfrlem16  8409  1oex  8494  naddunif  8711  mapsnd  8922  fvdiagfn  8927  mapsnconst  8928  mapsncnv  8929  mapsnf1o2  8930  ralxpmap  8932  elixpsn  8973  ixpsnf1o  8974  mapsnf1o  8975  ensn1  9056  2dom  9066  mapsnend  9072  snmapen  9074  en2sn  9077  xpsnen  9088  endisj  9091  xpsnen2g  9097  domunsncan  9104  enfixsn  9113  disjenex  9162  domssex2  9164  domssex  9165  map2xp  9174  pssnn  9192  snnen2o  9244  isinf  9264  ac6sfi  9283  fczfsuppd  9385  snopfsupp  9390  fisn  9426  tc2  9748  tcsni  9749  ranksuc  9889  hfsnOLD  9928  djuex  9996  fseqenlem1  10110  djuassen  10264  mapdjuen  10266  djudom1  10268  djuinf  10274  ackbij1lem5  10308  cfsuc  10342  dcomex  10532  axdc3lem4  10538  axdc4lem  10540  ttukeylem3  10596  brdom7disj  10617  brdom6disj  10618  fpwwe2lem12  10734  nn0ex  12619  hashxplem  14585  hashf1lem1  14607  hashge3el3dif  14639  ofs1  15132  climconst2  15724  ramub1lem2  17214  cshwsex  17287  setsvalg  17353  setsid  17394  pwsbas  17667  pwsle  17673  pwssca  17677  pwssnf1o  17679  imasplusg  17698  imasmulr  17699  imasvsca  17701  imasip  17702  acsfn  17842  homaval  18215  funcsetcestrclem1  18337  mgm1  18845  sgrp1  18927  mnd1  18982  mnd1id  18983  efmnd1bas  19098  idresefmnd  19104  smndex1gbas  19107  smndex1gid  19109  smndex1igid  19111  smndex1bas  19114  smndex1sgrp  19116  smndex1mnd  19118  smndex1id  19119  grp1  19266  grp1inv  19267  mulgfval  19288  triv1nsgd  19392  1nsgtrivd  19393  symg2bas  19616  idrespermg  19634  pmtrsn  19742  psgnsn  19743  abl1  20089  dprdz  20255  dprdsn  20261  simpgnsgd  20325  2nsgsimpgd  20327  ring1  20550  rng1nnzr  21042  pwssplit3  21345  lpival  21657  cnfldex  21690  pzriprnglem13  21808  pzriprnglem14  21809  frlmip  22093  islindf4  22153  evlsvvval  22411  evlssca  22412  evlsevl  22450  psdmul  22496  evls1sca  22650  mattposvs  22779  mat1dimelbas  22795  mat1dimscm  22799  mat1dimmul  22800  mat1rhmval  22803  m1detdiag  22921  mdetrlin  22926  mdetrsca2  22928  mdetrlin2  22931  mdetunilem5  22940  smadiadetglem2  22996  basdif0  23280  ordtbas  23519  leordtval2  23539  conncompid  23758  ptbasfi  23909  dfac14lem  23945  dfac14  23946  ptrescn  23967  xkoptsub  23982  pt1hmeo  24134  xpstopnlem1  24137  ufileu  24247  filufint  24248  uffix  24249  uffixsn  24253  flimclslem  24312  ptcmplem1  24380  imasdsf1olem  24701  icccmplem1  25151  icccmplem2  25152  rrxip  25720  rrxsca  25726  ehl1eudis  25750  elply2  26523  plyss  26526  plyeq0lem  26538  taylfval  26695  sltssnb  28164  lesrec  28194  eqcuts3  28199  0lt1s  28207  sltsleft  28255  sltsright  28256  addsval  28357  addsuniflem  28396  negsid  28436  negsunif  28450  mulsval  28504  sltmuls1  28542  sltmuls2  28543  precsexlem1  28602  precsexlem2  28603  precsexlem11  28612  n0fincut  28750  axlowdimlem15  29543  axlowdim  29548  snstriedgval  29625  vtxvalsnop  29628  iedgvalsnop  29629  upgr1eop  29702  upgr1eopALT  29704  uspgr1eop  29837  usgr1eop  29840  1loopgrvd2  30093  1loopgrvd0  30094  p1evtxdeqlem  30102  p1evtxdeq  30103  p1evtxdp1  30104  uspgrloopvtx  30105  uspgrloopiedg  30107  uspgrloopedg  30108  wlkp1lem4  30264  0pthonv  30729  eupth2lem3  30846  wlkl0  30977  0ofval  31398  suppovss  33325  padct  33361  resf1o  33372  elrgspnlem4  33856  elrspunsn  34029  drngidlhash  34033  fldlring  34081  0mplrim  34196  selvply1rhmlema  34200  selvply1rhmlemb  34201  selvply1rhmlem1  34202  selvply1rhmlem2  34203  selvply1rhmlem4  34205  zar0ring  34560  ordtconnlem1  34606  esumpr  34748  esumrnmpt2  34750  esumfzf  34751  prsiga  34813  rossros  34863  cntnevol  34911  omsmeas  35005  ccatmulgnn0dir  35224  ofcs1  35226  actfunsnf1o  35283  actfunsnrndisj  35284  reprsuc  35294  breprexplema  35309  bnj918  35447  bnj95  35544  bnj1489  35736  fineqvac  35852  kard0  35890  kardsn  35896  subfacp1lem5  36067  erdszelem5  36078  erdszelem8  36081  cvmliftlem4  36171  cvmliftlem5  36172  cvmlift2lem6  36191  cvmlift2lem9  36194  cvmlift2lem12  36197  satfv1lem  36245  prv1n  36314  brapply  36824  lemsuccf  36827  altopthsn  36850  neibastop2lem  37272  topjoin  37277  onpsstopbas  37342  weiunse  37380  ttcsnexg  37432  bj-2uplex  38059  bj-restsn  38139  finixpnum  38665  ptrest  38674  poimirlem3  38678  poimirlem4  38679  poimirlem28  38703  dfproplem  38778  fdc  38816  heiborlem8  38889  ismrer1  38909  grposnOLD  38953  zrdivrng  39024  lsatset  40184  ldualset  40319  lineset  40932  dvaset  42199  dvhset  42275  dibval  42336  dibfna  42348  sticksstones9  43341  frlmsnic  43741  elrfi  43842  wopprc  44174  dfac11  44201  kelac2  44204  safesnsupfidom1o  44555  sn1dom  44664  pr2dom  44665  tr3dom  44666  fvilbdRP  44827  brtrclfv2  44864  frege110  45110  frege133  45133  k0004lem3  45286  mnuprdlem1  45393  mnuprdlem2  45394  mnuprdlem3  45395  snelpwrVD  45949  nregmodelf1o  46141  fnchoice  46182  elmapsnd  46354  difmapsn  46361  unirnmapsn  46363  ssmapsn  46365  limcresiooub  46788  limcresioolb  46789  cnfdmsn  47028  dvsinax  47059  fourierdlem48  47300  fourierdlem49  47301  sge0sn  47525  sge0p1  47560  hoicvr  47694  ovnovollem1  47802  ovnovollem2  47803  vonvolmbllem  47806  numtowerdt  48052  fsetsnf  48257  fsetsnf1  48258  fsetsnfo  48259  cfsetsnfsetfo  48266  setsv  48596  nnsum3primesprm  49024  mapsnop  49592  lindsrng01  49716  snlindsntorlem  49718  snlindsntor  49719  lmod1lem1  49735  lmod1lem2  49736  lmod1lem3  49737  lmod1lem4  49738  lmod1lem5  49739  lmod1  49740  lmod1zr  49741  fv1arycl  49885  1arympt1fv  49887  1arymaptfo  49891  eufsn2  50090  discsubclem  50313  discsubc  50314  iinfconstbas  50316  diag1f1lem  50564  setcsnterm  50761  setc1ocofval  50765  isinito2lem  50769  idfudiag1  50796  diag1f1olem  50804  prstchomval  50833  mndtcbasval  50854  mndtchom  50858  mndtcco  50859  incat  50875  setc1onsubc  50876  parhomval  50879  parhomidval  50882  parcatid2  50899  parcatid  50900  parmapfunc2  50910  aacllem  51150