Theorem snex 5375

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 5322. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.)

Assertion

Ref	Expression
snex	⊢ {𝐴} ∈ V

Proof of Theorem snex

Step	Hyp	Ref	Expression
1		snexg 5374	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
2		snprc 4669	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
3	2	biimpi 216	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴} = ∅)
4		0ex 5246	. . 3 ⊢ ∅ ∈ V
5	3, 4	eqeltrdi 2836	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ V)
6	1, 5	pm2.61i 182	1 ⊢ {𝐴} ∈ V

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2109  Vcvv 3436  ∅c0 4284  {csn 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-dif 3906  df-un 3908  df-nul 4285  df-sn 4578  df-pr 4580

This theorem is referenced by:  prex  5376  snelpwiOLD  5387  intidOLD  5401  elopg  5409  opi1  5411  op1stb  5414  opnz  5416  opeqsng  5446  opeqpr  5448  snopeqop  5449  opthwiener  5457  uniop  5458  0sn0ep  5523  frirr  5595  opthprc  5683  frsn  5707  relop  5793  snsn0non  6433  onnev  6435  funsneqopb  7086  fsnex  7220  tpex  7682  difsnexi  7697  sucexb  7740  elxp4  7855  elxp5  7856  fvclex  7894  1stval  7926  2ndval  7927  fnse  8066  suppsnop  8111  brtpos2  8165  frrlem13  8231  tfrlem12  8311  tfrlem16  8315  1oex  8398  naddunif  8611  mapsnd  8813  fvdiagfn  8818  mapsnconst  8819  mapsncnv  8820  mapsnf1o2  8821  ralxpmap  8823  elixpsn  8864  ixpsnf1o  8865  mapsnf1o  8866  ensn1  8946  2dom  8955  mapsnend  8961  snmapen  8963  en2sn  8966  xpsnen  8978  endisj  8981  xpsnen2g  8987  domunsncan  8994  enfixsn  9003  disjenex  9052  domssex2  9054  domssex  9055  map2xp  9064  pssnn  9082  snnen2o  9134  isinf  9154  ac6sfi  9173  fodomfiOLD  9220  fczfsuppd  9276  snopfsupp  9281  fisn  9317  tc2  9638  tcsni  9639  ranksuc  9761  djuex  9804  fseqenlem1  9918  djuassen  10073  mapdjuen  10075  djudom1  10077  djuinf  10083  ackbij1lem5  10117  cfsuc  10151  dcomex  10341  axdc3lem4  10347  axdc4lem  10349  ttukeylem3  10405  brdom7disj  10425  brdom6disj  10426  fpwwe2lem12  10536  nn0ex  12390  hashxplem  14340  hashf1lem1  14362  hashge3el3dif  14394  ofs1  14877  climconst2  15455  ramub1lem2  16939  cshwsex  17012  setsvalg  17077  setsid  17118  pwsbas  17391  pwsle  17396  pwssca  17400  pwssnf1o  17402  imasplusg  17421  imasmulr  17422  imasvsca  17424  imasip  17425  acsfn  17565  homaval  17938  funcsetcestrclem1  18060  mgm1  18532  sgrp1  18603  mnd1  18653  mnd1id  18654  efmnd1bas  18767  idresefmnd  18773  smndex1bas  18780  smndex1sgrp  18782  smndex1mnd  18784  smndex1id  18785  grp1  18926  grp1inv  18927  mulgfval  18948  triv1nsgd  19052  1nsgtrivd  19053  symg2bas  19272  idrespermg  19290  pmtrsn  19398  psgnsn  19399  abl1  19745  dprdz  19911  dprdsn  19917  simpgnsgd  19981  2nsgsimpgd  19983  ring1  20195  rng1nnzr  20660  pwssplit3  20965  cnfldex  21264  pzriprnglem13  21400  pzriprnglem14  21401  frlmip  21685  islindf4  21745  evlssca  21994  psdmul  22051  evls1sca  22208  mattposvs  22340  mat1dimelbas  22356  mat1dimscm  22360  mat1dimmul  22361  mat1rhmval  22364  m1detdiag  22482  mdetrlin  22487  mdetrsca2  22489  mdetrlin2  22492  mdetunilem5  22501  smadiadetglem2  22557  basdif0  22838  ordtbas  23077  leordtval2  23097  conncompid  23316  ptbasfi  23466  dfac14lem  23502  dfac14  23503  ptrescn  23524  xkoptsub  23539  pt1hmeo  23691  xpstopnlem1  23694  ufileu  23804  filufint  23805  uffix  23806  uffixsn  23810  flimclslem  23869  ptcmplem1  23937  imasdsf1olem  24259  icccmplem1  24709  icccmplem2  24710  rrxip  25288  rrxsca  25294  ehl1eudis  25318  elply2  26099  plyss  26102  plyeq0lem  26113  taylfval  26264  ssltsn  27703  slerec  27730  eqscut3  27735  0slt1s  27743  ssltleft  27784  ssltright  27785  addsval  27874  addsuniflem  27913  negsid  27952  negsunif  27966  mulsval  28017  ssltmul1  28055  ssltmul2  28056  precsexlem1  28114  precsexlem2  28115  precsexlem11  28124  n0sfincut  28251  0reno  28366  axlowdimlem15  28901  axlowdim  28906  snstriedgval  28983  vtxvalsnop  28986  iedgvalsnop  28987  upgr1eop  29060  upgr1eopALT  29062  uspgr1eop  29192  usgr1eop  29195  1loopgrvd2  29449  1loopgrvd0  29450  p1evtxdeqlem  29458  p1evtxdeq  29459  p1evtxdp1  29460  uspgrloopvtx  29461  uspgrloopiedg  29463  uspgrloopedg  29464  wlkp1lem4  29620  0pthonv  30073  eupth2lem3  30180  wlkl0  30311  0ofval  30731  suppovss  32623  resf1o  32673  elrgspnlem4  33185  elrspunsn  33366  drngidlhash  33371  zar0ring  33845  ordtconnlem1  33891  esumpr  34033  esumrnmpt2  34035  esumfzf  34036  prsiga  34098  rossros  34147  cntnevol  34195  omsmeas  34291  ccatmulgnn0dir  34510  ofcs1  34512  actfunsnf1o  34572  actfunsnrndisj  34573  reprsuc  34583  breprexplema  34598  bnj918  34733  bnj95  34831  bnj1489  35023  fineqvac  35072  subfacp1lem5  35157  erdszelem5  35168  erdszelem8  35171  cvmliftlem4  35261  cvmliftlem5  35262  cvmlift2lem6  35281  cvmlift2lem9  35284  cvmlift2lem12  35287  satfv1lem  35335  prv1n  35404  brapply  35912  brsuccf  35915  altopthsn  35935  hfsn  36153  neibastop2lem  36334  topjoin  36339  onpsstopbas  36404  weiunse  36442  bj-2uplex  36996  bj-restsn  37056  finixpnum  37585  ptrest  37599  poimirlem3  37603  poimirlem4  37604  poimirlem28  37628  fdc  37725  heiborlem8  37798  ismrer1  37818  grposnOLD  37862  zrdivrng  37933  ldualset  39104  lineset  39717  dvaset  40984  dvhset  41060  dibval  41121  dibfna  41133  sticksstones9  42127  frlmsnic  42513  evlsvvval  42536  evlsevl  42544  elrfi  42667  wopprc  43003  dfac11  43035  kelac2  43038  safesnsupfidom1o  43390  sn1dom  43499  pr2dom  43500  tr3dom  43501  fvilbdRP  43663  brtrclfv2  43700  frege110  43946  frege133  43969  k0004lem3  44122  mnuprdlem1  44245  mnuprdlem2  44246  snelpwrVD  44804  nregmodelf1o  44989  fnchoice  45007  elmapsnd  45182  difmapsn  45190  unirnmapsn  45192  ssmapsn  45194  limcresiooub  45623  limcresioolb  45624  cnfdmsn  45863  dvsinax  45894  fourierdlem48  46135  fourierdlem49  46136  sge0sn  46360  sge0p1  46395  ovnovollem1  46637  ovnovollem2  46638  vonvolmbllem  46641  fsetsnf  47035  fsetsnf1  47036  fsetsnfo  47037  cfsetsnfsetfo  47044  setsv  47362  nnsum3primesprm  47774  mapsnop  48328  lindsrng01  48453  snlindsntorlem  48455  snlindsntor  48456  lmod1lem1  48472  lmod1lem2  48473  lmod1lem3  48474  lmod1lem4  48475  lmod1lem5  48476  lmod1  48477  lmod1zr  48478  fv1arycl  48622  1arympt1fv  48624  1arymaptfo  48628  eufsn2  48827  discsubclem  49048  discsubc  49049  iinfconstbas  49051  diag1f1lem  49291  setcsnterm  49475  setc1ocofval  49479  isinito2lem  49483  idfudiag1  49510  diag1f1olem  49518  prstchomval  49544  mndtcbasval  49565  mndtchom  49569  mndtcco  49570  incat  49586  setc1onsubc  49587  aacllem  49786