Theorem snex 5404

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

This proof depends on syntax axioms:   ∈ wcel 2145  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 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  snexg  5405  elopg  5442  opi1  5444  op1stb  5447  opnz  5449  opeqsng  5480  opeqpr  5482  snopeqop  5483  opthwiener  5491  uniop  5492  0sn0ep  5559  frirr  5631  opthprc  5719  frsn  5743  relop  5830  snsn0non  6484  onnev  6486  funsneqopb  7149  fsnex  7284  tpex  7747  difsnexi  7760  sucexb  7803  elxp4  7919  elxp5  7920  fvclex  7956  1stval  7988  2ndval  7989  fnse  8131  suppsnop  8176  brtpos2  8230  frrlem13  8297  tfrlem12  8378  tfrlem16  8382  1oex  8465  naddunif  8682  mapsnd  8893  fvdiagfn  8898  mapsnconst  8899  mapsncnv  8900  mapsnf1o2  8901  ralxpmap  8903  elixpsn  8944  ixpsnf1o  8945  mapsnf1o  8946  ensn1  9027  2dom  9037  mapsnend  9043  snmapen  9045  en2sn  9048  xpsnen  9059  endisj  9062  xpsnen2g  9068  domunsncan  9075  enfixsn  9084  disjenex  9133  domssex2  9135  domssex  9136  map2xp  9145  pssnn  9163  snnen2o  9215  isinf  9235  ac6sfi  9254  fczfsuppd  9356  snopfsupp  9361  fisn  9397  tc2  9719  tcsni  9720  ranksuc  9847  djuex  9913  fseqenlem1  10027  djuassen  10181  mapdjuen  10183  djudom1  10185  djuinf  10191  ackbij1lem5  10225  cfsuc  10259  dcomex  10449  axdc3lem4  10455  axdc4lem  10457  ttukeylem3  10513  brdom7disj  10534  brdom6disj  10535  fpwwe2lem12  10651  nn0ex  12534  hashxplem  14498  hashf1lem1  14520  hashge3el3dif  14552  ofs1  15043  climconst2  15635  ramub1lem2  17119  cshwsex  17192  setsvalg  17258  setsid  17299  pwsbas  17572  pwsle  17578  pwssca  17582  pwssnf1o  17584  imasplusg  17603  imasmulr  17604  imasvsca  17606  imasip  17607  acsfn  17747  homaval  18120  funcsetcestrclem1  18242  mgm1  18750  sgrp1  18831  mnd1  18886  mnd1id  18887  efmnd1bas  19002  idresefmnd  19008  smndex1gbas  19011  smndex1gid  19013  smndex1igid  19015  smndex1bas  19018  smndex1sgrp  19020  smndex1mnd  19022  smndex1id  19023  grp1  19170  grp1inv  19171  mulgfval  19192  triv1nsgd  19296  1nsgtrivd  19297  symg2bas  19520  idrespermg  19538  pmtrsn  19646  psgnsn  19647  abl1  19993  dprdz  20159  dprdsn  20165  simpgnsgd  20229  2nsgsimpgd  20231  ring1  20452  rng1nnzr  20942  pwssplit3  21245  lpival  21555  cnfldex  21588  pzriprnglem13  21706  pzriprnglem14  21707  frlmip  21991  islindf4  22051  evlsvvval  22309  evlssca  22310  evlsevl  22348  psdmul  22394  evls1sca  22548  mattposvs  22677  mat1dimelbas  22693  mat1dimscm  22697  mat1dimmul  22698  mat1rhmval  22701  m1detdiag  22819  mdetrlin  22824  mdetrsca2  22826  mdetrlin2  22829  mdetunilem5  22838  smadiadetglem2  22894  basdif0  23178  ordtbas  23417  leordtval2  23437  conncompid  23656  ptbasfi  23807  dfac14lem  23843  dfac14  23844  ptrescn  23865  xkoptsub  23880  pt1hmeo  24032  xpstopnlem1  24035  ufileu  24145  filufint  24146  uffix  24147  uffixsn  24151  flimclslem  24210  ptcmplem1  24278  imasdsf1olem  24599  icccmplem1  25049  icccmplem2  25050  rrxip  25618  rrxsca  25624  ehl1eudis  25648  elply2  26421  plyss  26424  plyeq0lem  26436  taylfval  26595  sltssnb  28034  lesrec  28064  eqcuts3  28069  0lt1s  28077  sltsleft  28125  sltsright  28126  addsval  28227  addsuniflem  28266  negsid  28306  negsunif  28320  mulsval  28374  sltmuls1  28412  sltmuls2  28413  precsexlem1  28472  precsexlem2  28473  precsexlem11  28482  n0fincut  28620  axlowdimlem15  29413  axlowdim  29418  snstriedgval  29495  vtxvalsnop  29498  iedgvalsnop  29499  upgr1eop  29572  upgr1eopALT  29574  uspgr1eop  29707  usgr1eop  29710  1loopgrvd2  29963  1loopgrvd0  29964  p1evtxdeqlem  29972  p1evtxdeq  29973  p1evtxdp1  29974  uspgrloopvtx  29975  uspgrloopiedg  29977  uspgrloopedg  29978  wlkp1lem4  30134  0pthonv  30599  eupth2lem3  30716  wlkl0  30847  0ofval  31268  suppovss  33153  padct  33189  resf1o  33201  elrgspnlem4  33685  elrspunsn  33857  drngidlhash  33861  fldlring  33909  0mplrim  34024  selvply1rhmlema  34028  selvply1rhmlemb  34029  selvply1rhmlem1  34030  selvply1rhmlem2  34031  selvply1rhmlem4  34033  zar0ring  34388  ordtconnlem1  34434  esumpr  34576  esumrnmpt2  34578  esumfzf  34579  prsiga  34641  rossros  34691  cntnevol  34739  omsmeas  34834  ccatmulgnn0dir  35053  ofcs1  35055  actfunsnf1o  35112  actfunsnrndisj  35113  reprsuc  35123  breprexplema  35138  bnj918  35276  bnj95  35373  bnj1489  35565  fineqvac  35642  kard0  35680  kardsn  35686  subfacp1lem5  35763  erdszelem5  35774  erdszelem8  35777  cvmliftlem4  35867  cvmliftlem5  35868  cvmlift2lem6  35887  cvmlift2lem9  35890  cvmlift2lem12  35893  satfv1lem  35941  prv1n  36010  brapply  36515  lemsuccf  36518  altopthsn  36541  hfsn  36759  neibastop2lem  36979  topjoin  36984  onpsstopbas  37049  weiunse  37087  ttcsnexg  37139  bj-2uplex  37766  bj-restsn  37832  finixpnum  38359  ptrest  38368  poimirlem3  38372  poimirlem4  38373  poimirlem28  38397  fdc  38495  heiborlem8  38568  ismrer1  38588  grposnOLD  38632  zrdivrng  38703  lsatset  39863  ldualset  39998  lineset  40611  dvaset  41878  dvhset  41954  dibval  42015  dibfna  42027  sticksstones9  43020  frlmsnic  43422  elrfi  43539  wopprc  43871  dfac11  43903  kelac2  43906  safesnsupfidom1o  44257  sn1dom  44366  pr2dom  44367  tr3dom  44368  fvilbdRP  44530  brtrclfv2  44567  frege110  44813  frege133  44836  k0004lem3  44989  mnuprdlem1  45096  mnuprdlem2  45097  mnuprdlem3  45098  snelpwrVD  45653  nregmodelf1o  45838  fnchoice  45863  elmapsnd  46035  difmapsn  46042  unirnmapsn  46044  ssmapsn  46046  limcresiooub  46470  limcresioolb  46471  cnfdmsn  46710  dvsinax  46741  fourierdlem48  46982  fourierdlem49  46983  sge0sn  47207  sge0p1  47242  hoicvr  47376  ovnovollem1  47484  ovnovollem2  47485  vonvolmbllem  47488  numtowerdt  47734  fsetsnf  47939  fsetsnf1  47940  fsetsnfo  47941  cfsetsnfsetfo  47948  setsv  48278  nnsum3primesprm  48706  mapsnop  49274  lindsrng01  49398  snlindsntorlem  49400  snlindsntor  49401  lmod1lem1  49417  lmod1lem2  49418  lmod1lem3  49419  lmod1lem4  49420  lmod1lem5  49421  lmod1  49422  lmod1zr  49423  fv1arycl  49567  1arympt1fv  49569  1arymaptfo  49573  eufsn2  49771  discsubclem  49989  discsubc  49990  iinfconstbas  49992  diag1f1lem  50232  setcsnterm  50416  setc1ocofval  50420  isinito2lem  50424  idfudiag1  50451  diag1f1olem  50459  prstchomval  50485  mndtcbasval  50506  mndtchom  50510  mndtcco  50511  incat  50527  setc1onsubc  50528  aacllem  50772