Theorem snex 5396

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  {csn 4583  {cpr 4585

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 5390

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 4151  df-sn 4584  df-pr 4586

This theorem is used by:  snexg  5397  elopg  5434  opi1  5436  op1stb  5439  opnz  5441  opeqsng  5474  opeqpr  5476  snopeqop  5477  opthwiener  5486  uniop  5487  0sn0ep  5554  frirr  5626  opthprc  5714  frsn  5738  relop  5827  snsn0non  6489  onnev  6491  funsneqopb  7156  fsnex  7291  tpex  7762  difsnexi  7775  sucexb  7818  elxp4  7934  elxp5  7935  fvclex  7971  1stval  8003  2ndval  8004  fnse  8150  suppsnop  8196  brtpos2  8250  frrlem13  8317  tfrlem12  8398  tfrlem16  8402  1oex  8487  naddunif  8704  mapsnd  8915  fvdiagfn  8920  mapsnconst  8921  mapsncnv  8922  mapsnf1o2  8923  ralxpmap  8925  elixpsn  8966  ixpsnf1o  8967  mapsnf1o  8968  ensn1  9049  2dom  9059  mapsnend  9065  snmapen  9067  en2sn  9070  xpsnen  9081  endisj  9084  xpsnen2g  9090  domunsncan  9097  enfixsn  9106  disjenex  9155  domssex2  9157  domssex  9158  map2xp  9167  pssnn  9185  snnen2o  9237  isinf  9257  ac6sfi  9276  fczfsuppd  9379  snopfsupp  9384  fisn  9420  tc2  9742  tcsni  9743  ranksuc  9883  hfsnOLD  9922  djuex  9990  fseqenlem1  10104  djuassen  10258  mapdjuen  10260  djudom1  10262  djuinf  10268  ackbij1lem5  10302  cfsuc  10336  dcomex  10526  axdc3lem4  10532  axdc4lem  10534  ttukeylem3  10590  brdom7disj  10611  brdom6disj  10612  fpwwe2lem12  10728  nn0ex  12613  hashxplem  14579  hashf1lem1  14601  hashge3el3dif  14633  ofs1  15124  climconst2  15716  ramub1lem2  17206  cshwsex  17279  setsvalg  17345  setsid  17386  pwsbas  17659  pwsle  17665  pwssca  17669  pwssnf1o  17671  imasplusg  17690  imasmulr  17691  imasvsca  17693  imasip  17694  acsfn  17834  homaval  18207  funcsetcestrclem1  18329  mgm1  18837  sgrp1  18919  mnd1  18974  mnd1id  18975  efmnd1bas  19090  idresefmnd  19096  smndex1gbas  19099  smndex1gid  19101  smndex1igid  19103  smndex1bas  19106  smndex1sgrp  19108  smndex1mnd  19110  smndex1id  19111  grp1  19258  grp1inv  19259  mulgfval  19280  triv1nsgd  19384  1nsgtrivd  19385  symg2bas  19608  idrespermg  19626  pmtrsn  19734  psgnsn  19735  abl1  20081  dprdz  20247  dprdsn  20253  simpgnsgd  20317  2nsgsimpgd  20319  ring1  20542  rng1nnzr  21034  pwssplit3  21337  lpival  21649  cnfldex  21682  pzriprnglem13  21800  pzriprnglem14  21801  frlmip  22085  islindf4  22145  evlsvvval  22403  evlssca  22404  evlsevl  22442  psdmul  22488  evls1sca  22642  mattposvs  22771  mat1dimelbas  22787  mat1dimscm  22791  mat1dimmul  22792  mat1rhmval  22795  m1detdiag  22913  mdetrlin  22918  mdetrsca2  22920  mdetrlin2  22923  mdetunilem5  22932  smadiadetglem2  22988  basdif0  23272  ordtbas  23511  leordtval2  23531  conncompid  23750  ptbasfi  23901  dfac14lem  23937  dfac14  23938  ptrescn  23959  xkoptsub  23974  pt1hmeo  24126  xpstopnlem1  24129  ufileu  24239  filufint  24240  uffix  24241  uffixsn  24245  flimclslem  24304  ptcmplem1  24372  imasdsf1olem  24693  icccmplem1  25143  icccmplem2  25144  rrxip  25712  rrxsca  25718  ehl1eudis  25742  elply2  26515  plyss  26518  plyeq0lem  26530  taylfval  26687  sltssnb  28156  lesrec  28186  eqcuts3  28191  0lt1s  28199  sltsleft  28247  sltsright  28248  addsval  28349  addsuniflem  28388  negsid  28428  negsunif  28442  mulsval  28496  sltmuls1  28534  sltmuls2  28535  precsexlem1  28594  precsexlem2  28595  precsexlem11  28604  n0fincut  28742  axlowdimlem15  29535  axlowdim  29540  snstriedgval  29617  vtxvalsnop  29620  iedgvalsnop  29621  upgr1eop  29694  upgr1eopALT  29696  uspgr1eop  29829  usgr1eop  29832  1loopgrvd2  30085  1loopgrvd0  30086  p1evtxdeqlem  30094  p1evtxdeq  30095  p1evtxdp1  30096  uspgrloopvtx  30097  uspgrloopiedg  30099  uspgrloopedg  30100  wlkp1lem4  30256  0pthonv  30721  eupth2lem3  30838  wlkl0  30969  0ofval  31390  suppovss  33317  padct  33353  resf1o  33365  elrgspnlem4  33849  elrspunsn  34022  drngidlhash  34026  fldlring  34074  0mplrim  34189  selvply1rhmlema  34193  selvply1rhmlemb  34194  selvply1rhmlem1  34195  selvply1rhmlem2  34196  selvply1rhmlem4  34198  zar0ring  34553  ordtconnlem1  34599  esumpr  34741  esumrnmpt2  34743  esumfzf  34744  prsiga  34806  rossros  34856  cntnevol  34904  omsmeas  34998  ccatmulgnn0dir  35217  ofcs1  35219  actfunsnf1o  35276  actfunsnrndisj  35277  reprsuc  35287  breprexplema  35302  bnj918  35440  bnj95  35537  bnj1489  35729  fineqvac  35833  kard0  35871  kardsn  35877  subfacp1lem5  36018  erdszelem5  36029  erdszelem8  36032  cvmliftlem4  36122  cvmliftlem5  36123  cvmlift2lem6  36142  cvmlift2lem9  36145  cvmlift2lem12  36148  satfv1lem  36196  prv1n  36265  brapply  36775  lemsuccf  36778  altopthsn  36801  neibastop2lem  37223  topjoin  37228  onpsstopbas  37293  weiunse  37331  ttcsnexg  37383  bj-2uplex  38010  bj-restsn  38078  finixpnum  38604  ptrest  38613  poimirlem3  38617  poimirlem4  38618  poimirlem28  38642  dfproplem  38717  fdc  38755  heiborlem8  38828  ismrer1  38848  grposnOLD  38892  zrdivrng  38963  lsatset  40123  ldualset  40258  lineset  40871  dvaset  42138  dvhset  42214  dibval  42275  dibfna  42287  sticksstones9  43280  frlmsnic  43680  elrfi  43781  wopprc  44113  dfac11  44140  kelac2  44143  safesnsupfidom1o  44494  sn1dom  44603  pr2dom  44604  tr3dom  44605  fvilbdRP  44766  brtrclfv2  44803  frege110  45049  frege133  45072  k0004lem3  45225  mnuprdlem1  45332  mnuprdlem2  45333  mnuprdlem3  45334  snelpwrVD  45889  nregmodelf1o  46081  fnchoice  46122  elmapsnd  46294  difmapsn  46301  unirnmapsn  46303  ssmapsn  46305  limcresiooub  46728  limcresioolb  46729  cnfdmsn  46968  dvsinax  46999  fourierdlem48  47240  fourierdlem49  47241  sge0sn  47465  sge0p1  47500  hoicvr  47634  ovnovollem1  47742  ovnovollem2  47743  vonvolmbllem  47746  numtowerdt  47992  fsetsnf  48197  fsetsnf1  48198  fsetsnfo  48199  cfsetsnfsetfo  48206  setsv  48536  nnsum3primesprm  48964  mapsnop  49532  lindsrng01  49656  snlindsntorlem  49658  snlindsntor  49659  lmod1lem1  49675  lmod1lem2  49676  lmod1lem3  49677  lmod1lem4  49678  lmod1lem5  49679  lmod1  49680  lmod1zr  49681  fv1arycl  49825  1arympt1fv  49827  1arymaptfo  49831  eufsn2  50029  discsubclem  50247  discsubc  50248  iinfconstbas  50250  diag1f1lem  50490  setcsnterm  50674  setc1ocofval  50678  isinito2lem  50682  idfudiag1  50709  diag1f1olem  50717  prstchomval  50743  mndtcbasval  50764  mndtchom  50768  mndtcco  50769  incat  50785  setc1onsubc  50786  aacllem  51015