Theorem snex 5381

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

Syntax hints:   ∈ wcel 2114  Vcvv 3429  {csn 4567  {cpr 4569

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-sn 4568  df-pr 4570

This theorem is referenced by:  snexg  5382  elopg  5419  opi1  5421  op1stb  5424  opnz  5426  opeqsng  5457  opeqpr  5459  snopeqop  5460  opthwiener  5468  uniop  5469  0sn0ep  5535  frirr  5607  opthprc  5695  frsn  5719  relop  5805  snsn0non  6449  onnev  6451  funsneqopb  7106  fsnex  7238  tpex  7700  difsnexi  7715  sucexb  7758  elxp4  7873  elxp5  7874  fvclex  7912  1stval  7944  2ndval  7945  fnse  8083  suppsnop  8128  brtpos2  8182  frrlem13  8248  tfrlem12  8328  tfrlem16  8332  1oex  8415  naddunif  8629  mapsnd  8834  fvdiagfn  8839  mapsnconst  8840  mapsncnv  8841  mapsnf1o2  8842  ralxpmap  8844  elixpsn  8885  ixpsnf1o  8886  mapsnf1o  8887  ensn1  8968  2dom  8977  mapsnend  8983  snmapen  8985  en2sn  8988  xpsnen  8999  endisj  9002  xpsnen2g  9008  domunsncan  9015  enfixsn  9024  disjenex  9073  domssex2  9075  domssex  9076  map2xp  9085  pssnn  9103  snnen2o  9155  isinf  9175  ac6sfi  9194  fodomfiOLD  9240  fczfsuppd  9299  snopfsupp  9304  fisn  9340  tc2  9661  tcsni  9662  ranksuc  9789  djuex  9832  fseqenlem1  9946  djuassen  10101  mapdjuen  10103  djudom1  10105  djuinf  10111  ackbij1lem5  10145  cfsuc  10179  dcomex  10369  axdc3lem4  10375  axdc4lem  10377  ttukeylem3  10433  brdom7disj  10453  brdom6disj  10454  fpwwe2lem12  10565  nn0ex  12443  hashxplem  14395  hashf1lem1  14417  hashge3el3dif  14449  ofs1  14932  climconst2  15510  ramub1lem2  16998  cshwsex  17071  setsvalg  17136  setsid  17177  pwsbas  17450  pwsle  17456  pwssca  17460  pwssnf1o  17462  imasplusg  17481  imasmulr  17482  imasvsca  17484  imasip  17485  acsfn  17625  homaval  17998  funcsetcestrclem1  18120  mgm1  18626  sgrp1  18697  mnd1  18747  mnd1id  18748  efmnd1bas  18861  idresefmnd  18867  smndex1gbas  18870  smndex1gid  18872  smndex1igid  18874  smndex1bas  18877  smndex1sgrp  18879  smndex1mnd  18881  smndex1id  18882  grp1  19023  grp1inv  19024  mulgfval  19045  triv1nsgd  19148  1nsgtrivd  19149  symg2bas  19368  idrespermg  19386  pmtrsn  19494  psgnsn  19495  abl1  19841  dprdz  20007  dprdsn  20013  simpgnsgd  20077  2nsgsimpgd  20079  ring1  20291  rng1nnzr  20752  pwssplit3  21056  lpival  21322  cnfldex  21355  pzriprnglem13  21473  pzriprnglem14  21474  frlmip  21758  islindf4  21818  evlsvvval  22071  evlssca  22072  psdmul  22132  evls1sca  22288  mattposvs  22420  mat1dimelbas  22436  mat1dimscm  22440  mat1dimmul  22441  mat1rhmval  22444  m1detdiag  22562  mdetrlin  22567  mdetrsca2  22569  mdetrlin2  22572  mdetunilem5  22581  smadiadetglem2  22637  basdif0  22918  ordtbas  23157  leordtval2  23177  conncompid  23396  ptbasfi  23546  dfac14lem  23582  dfac14  23583  ptrescn  23604  xkoptsub  23619  pt1hmeo  23771  xpstopnlem1  23774  ufileu  23884  filufint  23885  uffix  23886  uffixsn  23890  flimclslem  23949  ptcmplem1  24017  imasdsf1olem  24338  icccmplem1  24788  icccmplem2  24789  rrxip  25357  rrxsca  25363  ehl1eudis  25387  elply2  26161  plyss  26164  plyeq0lem  26175  taylfval  26324  sltssnb  27761  lesrec  27791  eqcuts3  27796  0lt1s  27804  sltsleft  27852  sltsright  27853  addsval  27954  addsuniflem  27993  negsid  28033  negsunif  28047  mulsval  28101  sltmuls1  28139  sltmuls2  28140  precsexlem1  28199  precsexlem2  28200  precsexlem11  28209  n0fincut  28347  axlowdimlem15  29025  axlowdim  29030  snstriedgval  29107  vtxvalsnop  29110  iedgvalsnop  29111  upgr1eop  29184  upgr1eopALT  29186  uspgr1eop  29316  usgr1eop  29319  1loopgrvd2  29572  1loopgrvd0  29573  p1evtxdeqlem  29581  p1evtxdeq  29582  p1evtxdp1  29583  uspgrloopvtx  29584  uspgrloopiedg  29586  uspgrloopedg  29587  wlkp1lem4  29743  0pthonv  30199  eupth2lem3  30306  wlkl0  30437  0ofval  30858  suppovss  32754  padct  32791  resf1o  32803  elrgspnlem4  33306  elrspunsn  33489  drngidlhash  33494  zar0ring  34022  ordtconnlem1  34068  esumpr  34210  esumrnmpt2  34212  esumfzf  34213  prsiga  34275  rossros  34324  cntnevol  34372  omsmeas  34467  ccatmulgnn0dir  34686  ofcs1  34688  actfunsnf1o  34748  actfunsnrndisj  34749  reprsuc  34759  breprexplema  34774  bnj918  34909  bnj95  35006  bnj1489  35198  fineqvac  35260  subfacp1lem5  35366  erdszelem5  35377  erdszelem8  35380  cvmliftlem4  35470  cvmliftlem5  35471  cvmlift2lem6  35490  cvmlift2lem9  35493  cvmlift2lem12  35496  satfv1lem  35544  prv1n  35613  brapply  36118  lemsuccf  36121  altopthsn  36143  hfsn  36361  neibastop2lem  36542  topjoin  36547  onpsstopbas  36612  weiunse  36650  ttcsnexg  36702  bj-2uplex  37329  bj-restsn  37394  finixpnum  37926  ptrest  37940  poimirlem3  37944  poimirlem4  37945  poimirlem28  37969  fdc  38066  heiborlem8  38139  ismrer1  38159  grposnOLD  38203  zrdivrng  38274  lsatset  39436  ldualset  39571  lineset  40184  dvaset  41451  dvhset  41527  dibval  41588  dibfna  41600  sticksstones9  42593  frlmsnic  42985  evlsevl  43007  elrfi  43126  wopprc  43458  dfac11  43490  kelac2  43493  safesnsupfidom1o  43844  sn1dom  43953  pr2dom  43954  tr3dom  43955  fvilbdRP  44117  brtrclfv2  44154  frege110  44400  frege133  44423  k0004lem3  44576  mnuprdlem1  44699  mnuprdlem2  44700  mnuprdlem3  44701  snelpwrVD  45257  nregmodelf1o  45442  fnchoice  45460  elmapsnd  45633  difmapsn  45641  unirnmapsn  45643  ssmapsn  45645  limcresiooub  46070  limcresioolb  46071  cnfdmsn  46310  dvsinax  46341  fourierdlem48  46582  fourierdlem49  46583  sge0sn  46807  sge0p1  46842  hoicvr  46976  ovnovollem1  47084  ovnovollem2  47085  vonvolmbllem  47088  nthrucw  47316  fsetsnf  47499  fsetsnf1  47500  fsetsnfo  47501  cfsetsnfsetfo  47508  setsv  47838  nnsum3primesprm  48266  mapsnop  48820  lindsrng01  48944  snlindsntorlem  48946  snlindsntor  48947  lmod1lem1  48963  lmod1lem2  48964  lmod1lem3  48965  lmod1lem4  48966  lmod1lem5  48967  lmod1  48968  lmod1zr  48969  fv1arycl  49113  1arympt1fv  49115  1arymaptfo  49119  eufsn2  49318  discsubclem  49538  discsubc  49539  iinfconstbas  49541  diag1f1lem  49781  setcsnterm  49965  setc1ocofval  49969  isinito2lem  49973  idfudiag1  50000  diag1f1olem  50008  prstchomval  50034  mndtcbasval  50055  mndtchom  50059  mndtcco  50060  incat  50076  setc1onsubc  50077  aacllem  50276