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 5340. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) Avoid ax-nul 5256 and shorten proof. (Revised by GG, 6-Mar-2026.)

Assertion

Ref	Expression
snex	⊢ {𝐴} ∈ V

Proof of Theorem snex

Step	Hyp	Ref	Expression
1		dfsn2 4595	. 2 ⊢ {𝐴} = {𝐴, 𝐴}
2		prex 5395	. 2 ⊢ {𝐴, 𝐴} ∈ V
3	1, 2	eqeltri 2858	1 ⊢ {𝐴} ∈ V

Syntax hints:   ∈ wcel 2142  Vcvv 3454  {csn 4582  {cpr 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-sn 4583  df-pr 4585

This theorem is referenced by:  snexg  5397  elopg  5434  opi1  5436  op1stb  5439  opnz  5441  opeqsng  5472  opeqpr  5474  snopeqop  5475  opthwiener  5483  uniop  5484  0sn0ep  5551  frirr  5623  opthprc  5711  frsn  5735  relop  5822  snsn0non  6472  onnev  6474  funsneqopb  7135  fsnex  7267  tpex  7729  difsnexi  7744  sucexb  7787  elxp4  7903  elxp5  7904  fvclex  7940  1stval  7972  2ndval  7973  fnse  8113  suppsnop  8158  brtpos2  8212  frrlem13  8279  tfrlem12  8360  tfrlem16  8364  1oex  8447  naddunif  8664  mapsnd  8868  fvdiagfn  8873  mapsnconst  8874  mapsncnv  8875  mapsnf1o2  8876  ralxpmap  8878  elixpsn  8919  ixpsnf1o  8920  mapsnf1o  8921  ensn1  9002  2dom  9011  mapsnend  9017  snmapen  9019  en2sn  9022  xpsnen  9033  endisj  9036  xpsnen2g  9042  domunsncan  9049  enfixsn  9058  disjenex  9107  domssex2  9109  domssex  9110  map2xp  9119  pssnn  9137  snnen2o  9189  isinf  9209  ac6sfi  9228  fczfsuppd  9332  snopfsupp  9337  fisn  9373  tc2  9695  tcsni  9696  ranksuc  9823  djuex  9866  fseqenlem1  9980  djuassen  10135  mapdjuen  10137  djudom1  10139  djuinf  10145  ackbij1lem5  10179  cfsuc  10214  dcomex  10404  axdc3lem4  10410  axdc4lem  10412  ttukeylem3  10468  brdom7disj  10488  brdom6disj  10489  fpwwe2lem12  10600  nn0ex  12487  hashxplem  14446  hashf1lem1  14468  hashge3el3dif  14500  ofs1  14983  climconst2  15575  ramub1lem2  17063  cshwsex  17136  setsvalg  17202  setsid  17243  pwsbas  17516  pwsle  17522  pwssca  17526  pwssnf1o  17528  imasplusg  17547  imasmulr  17548  imasvsca  17550  imasip  17551  acsfn  17691  homaval  18064  funcsetcestrclem1  18186  mgm1  18692  sgrp1  18763  mnd1  18813  mnd1id  18814  efmnd1bas  18927  idresefmnd  18933  smndex1gbas  18936  smndex1gid  18938  smndex1igid  18940  smndex1bas  18943  smndex1sgrp  18945  smndex1mnd  18947  smndex1id  18948  grp1  19089  grp1inv  19090  mulgfval  19111  triv1nsgd  19214  1nsgtrivd  19215  symg2bas  19433  idrespermg  19451  pmtrsn  19559  psgnsn  19560  abl1  19906  dprdz  20072  dprdsn  20078  simpgnsgd  20142  2nsgsimpgd  20144  ring1  20356  rng1nnzr  20821  pwssplit3  21125  lpival  21391  cnfldex  21424  pzriprnglem13  21542  pzriprnglem14  21543  frlmip  21827  islindf4  21887  evlsvvval  22143  evlssca  22144  evlsevl  22182  psdmul  22228  evls1sca  22383  mattposvs  22512  mat1dimelbas  22528  mat1dimscm  22532  mat1dimmul  22533  mat1rhmval  22536  m1detdiag  22654  mdetrlin  22659  mdetrsca2  22661  mdetrlin2  22664  mdetunilem5  22673  smadiadetglem2  22729  basdif0  23010  ordtbas  23249  leordtval2  23269  conncompid  23488  ptbasfi  23638  dfac14lem  23674  dfac14  23675  ptrescn  23696  xkoptsub  23711  pt1hmeo  23863  xpstopnlem1  23866  ufileu  23976  filufint  23977  uffix  23978  uffixsn  23982  flimclslem  24041  ptcmplem1  24109  imasdsf1olem  24430  icccmplem1  24880  icccmplem2  24881  rrxip  25449  rrxsca  25455  ehl1eudis  25479  elply2  26253  plyss  26256  plyeq0lem  26267  taylfval  26419  sltssnb  27859  lesrec  27889  eqcuts3  27894  0lt1s  27902  sltsleft  27950  sltsright  27951  addsval  28052  addsuniflem  28091  negsid  28131  negsunif  28145  mulsval  28199  sltmuls1  28237  sltmuls2  28238  precsexlem1  28297  precsexlem2  28298  precsexlem11  28307  n0fincut  28445  axlowdimlem15  29154  axlowdim  29159  snstriedgval  29236  vtxvalsnop  29239  iedgvalsnop  29240  upgr1eop  29313  upgr1eopALT  29315  uspgr1eop  29445  usgr1eop  29448  1loopgrvd2  29701  1loopgrvd0  29702  p1evtxdeqlem  29710  p1evtxdeq  29711  p1evtxdp1  29712  uspgrloopvtx  29713  uspgrloopiedg  29715  uspgrloopedg  29716  wlkp1lem4  29872  0pthonv  30328  eupth2lem3  30435  wlkl0  30566  0ofval  30987  suppovss  32880  padct  32917  resf1o  32929  elrgspnlem4  33423  elrspunsn  33612  drngidlhash  33617  fldlring  33692  0mplrim  33808  selvply1rhmlema  33812  selvply1rhmlemb  33813  selvply1rhmlem1  33814  selvply1rhmlem2  33815  selvply1rhmlem4  33817  zar0ring  34172  ordtconnlem1  34218  esumpr  34360  esumrnmpt2  34362  esumfzf  34363  prsiga  34425  rossros  34474  cntnevol  34522  omsmeas  34617  ccatmulgnn0dir  34836  ofcs1  34838  actfunsnf1o  34895  actfunsnrndisj  34896  reprsuc  34906  breprexplema  34921  bnj918  35059  bnj95  35156  bnj1489  35348  fineqvac  35409  subfacp1lem5  35531  erdszelem5  35542  erdszelem8  35545  cvmliftlem4  35635  cvmliftlem5  35636  cvmlift2lem6  35655  cvmlift2lem9  35658  cvmlift2lem12  35661  satfv1lem  35709  prv1n  35778  brapply  36283  lemsuccf  36286  altopthsn  36308  hfsn  36526  neibastop2lem  36717  topjoin  36722  onpsstopbas  36787  weiunse  36825  ttcsnexg  36877  bj-2uplex  37504  bj-restsn  37569  finixpnum  38101  ptrest  38115  poimirlem3  38119  poimirlem4  38120  poimirlem28  38144  fdc  38241  heiborlem8  38314  ismrer1  38334  grposnOLD  38378  zrdivrng  38449  lsatset  39611  ldualset  39746  lineset  40359  dvaset  41626  dvhset  41702  dibval  41763  dibfna  41775  sticksstones9  42768  frlmsnic  43155  elrfi  43272  wopprc  43604  dfac11  43636  kelac2  43639  safesnsupfidom1o  43990  sn1dom  44099  pr2dom  44100  tr3dom  44101  fvilbdRP  44263  brtrclfv2  44300  frege110  44546  frege133  44569  k0004lem3  44722  mnuprdlem1  44845  mnuprdlem2  44846  mnuprdlem3  44847  snelpwrVD  45403  nregmodelf1o  45588  fnchoice  45606  elmapsnd  45778  difmapsn  45785  unirnmapsn  45787  ssmapsn  45789  limcresiooub  46213  limcresioolb  46214  cnfdmsn  46453  dvsinax  46484  fourierdlem48  46725  fourierdlem49  46726  sge0sn  46950  sge0p1  46985  hoicvr  47119  ovnovollem1  47227  ovnovollem2  47228  vonvolmbllem  47231  nthrucw  47459  fsetsnf  47642  fsetsnf1  47643  fsetsnfo  47644  cfsetsnfsetfo  47651  setsv  47981  nnsum3primesprm  48409  mapsnop  48963  lindsrng01  49087  snlindsntorlem  49089  snlindsntor  49090  lmod1lem1  49106  lmod1lem2  49107  lmod1lem3  49108  lmod1lem4  49109  lmod1lem5  49110  lmod1  49111  lmod1zr  49112  fv1arycl  49256  1arympt1fv  49258  1arymaptfo  49262  eufsn2  49461  discsubclem  49681  discsubc  49682  iinfconstbas  49684  diag1f1lem  49924  setcsnterm  50108  setc1ocofval  50112  isinito2lem  50116  idfudiag1  50143  diag1f1olem  50151  prstchomval  50177  mndtcbasval  50198  mndtchom  50202  mndtcco  50203  incat  50219  setc1onsubc  50220  aacllem  50419