Theorem snex 5406

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 5353. (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 5405	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
2		snprc 4693	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
3	2	biimpi 216	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴} = ∅)
4		0ex 5277	. . 3 ⊢ ∅ ∈ V
5	3, 4	eqeltrdi 2842	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ V)
6	1, 5	pm2.61i 182	1 ⊢ {𝐴} ∈ V

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2108  Vcvv 3459  ∅c0 4308  {csn 4601

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-un 3931  df-nul 4309  df-sn 4602  df-pr 4604

This theorem is referenced by:  prex  5407  snelpwiOLD  5419  intidOLD  5433  elopg  5441  opi1  5443  op1stb  5446  opnz  5448  opeqsng  5478  opeqpr  5480  snopeqop  5481  opthwiener  5489  uniop  5490  0sn0ep  5557  frirr  5630  opthprc  5718  frsn  5742  relop  5830  snsn0non  6478  onnev  6480  funsneqopb  7141  fsnex  7275  tpex  7738  difsnexi  7753  sucexb  7796  elxp4  7916  elxp5  7917  fvclex  7955  1stval  7988  2ndval  7989  fnse  8130  suppsnop  8175  brtpos2  8229  frrlem13  8295  wfrlem15OLD  8335  tfrlem12  8401  tfrlem16  8405  1oex  8488  naddunif  8703  mapsnd  8898  fvdiagfn  8903  mapsnconst  8904  mapsncnv  8905  mapsnf1o2  8906  ralxpmap  8908  elixpsn  8949  ixpsnf1o  8950  mapsnf1o  8951  ensn1  9033  2dom  9042  mapsnend  9048  snmapen  9050  en2sn  9053  xpsnen  9067  endisj  9070  xpsnen2g  9077  domunsncan  9084  enfixsn  9093  disjenex  9147  domssex2  9149  domssex  9150  map2xp  9159  pssnn  9180  phplem2OLD  9227  snnen2o  9243  isinf  9266  isinfOLD  9267  ac6sfi  9290  xpfiOLD  9329  fodomfiOLD  9340  fczfsuppd  9396  snopfsupp  9401  fisn  9437  tc2  9754  tcsni  9755  ranksuc  9877  djuex  9920  fseqenlem1  10036  djuassen  10191  mapdjuen  10193  djudom1  10195  djuinf  10201  ackbij1lem5  10235  cfsuc  10269  dcomex  10459  axdc3lem4  10465  axdc4lem  10467  ttukeylem3  10523  brdom7disj  10543  brdom6disj  10544  fpwwe2lem12  10654  nn0ex  12505  hashxplem  14449  hashf1lem1  14471  hashge3el3dif  14503  ofs1  14987  climconst2  15562  ramub1lem2  17045  cshwsex  17118  setsvalg  17183  setsid  17224  pwsbas  17499  pwsle  17504  pwssca  17508  pwssnf1o  17510  imasplusg  17529  imasmulr  17530  imasvsca  17532  imasip  17533  acsfn  17669  homaval  18042  funcsetcestrclem1  18164  mgm1  18634  sgrp1  18705  mnd1  18755  mnd1id  18756  efmnd1bas  18869  idresefmnd  18875  smndex1bas  18882  smndex1sgrp  18884  smndex1mnd  18886  smndex1id  18887  grp1  19028  grp1inv  19029  mulgfval  19050  triv1nsgd  19154  1nsgtrivd  19155  symg2bas  19372  idrespermg  19390  pmtrsn  19498  psgnsn  19499  abl1  19845  dprdz  20011  dprdsn  20017  simpgnsgd  20081  2nsgsimpgd  20083  ring1  20268  rng1nnzr  20733  pwssplit3  21017  cnfldex  21316  pzriprnglem13  21452  pzriprnglem14  21453  frlmip  21736  islindf4  21796  evlssca  22045  psdmul  22102  evls1sca  22259  mattposvs  22391  mat1dimelbas  22407  mat1dimscm  22411  mat1dimmul  22412  mat1rhmval  22415  m1detdiag  22533  mdetrlin  22538  mdetrsca2  22540  mdetrlin2  22543  mdetunilem5  22552  smadiadetglem2  22608  basdif0  22889  ordtbas  23128  leordtval2  23148  conncompid  23367  ptbasfi  23517  dfac14lem  23553  dfac14  23554  ptrescn  23575  xkoptsub  23590  pt1hmeo  23742  xpstopnlem1  23745  ufileu  23855  filufint  23856  uffix  23857  uffixsn  23861  flimclslem  23920  ptcmplem1  23988  imasdsf1olem  24310  icccmplem1  24760  icccmplem2  24761  rrxip  25340  rrxsca  25346  ehl1eudis  25370  elply2  26151  plyss  26154  plyeq0lem  26165  taylfval  26316  ssltsn  27754  slerec  27781  0slt1s  27791  ssltleft  27826  ssltright  27827  addsval  27912  addsuniflem  27951  negsid  27990  negsunif  28004  mulsval  28052  ssltmul1  28090  ssltmul2  28091  precsexlem1  28148  precsexlem2  28149  precsexlem11  28158  nohalf  28324  0reno  28346  axlowdimlem15  28881  axlowdim  28886  snstriedgval  28963  vtxvalsnop  28966  iedgvalsnop  28967  upgr1eop  29040  upgr1eopALT  29042  uspgr1eop  29172  usgr1eop  29175  1loopgrvd2  29429  1loopgrvd0  29430  p1evtxdeqlem  29438  p1evtxdeq  29439  p1evtxdp1  29440  uspgrloopvtx  29441  uspgrloopiedg  29443  uspgrloopedg  29444  wlkp1lem4  29602  0pthonv  30056  eupth2lem3  30163  wlkl0  30294  0ofval  30714  suppovss  32604  resf1o  32653  elrgspnlem4  33186  elrspunsn  33390  drngidlhash  33395  zar0ring  33855  ordtconnlem1  33901  esumpr  34043  esumrnmpt2  34045  esumfzf  34046  prsiga  34108  rossros  34157  cntnevol  34205  omsmeas  34301  ccatmulgnn0dir  34520  ofcs1  34522  actfunsnf1o  34582  actfunsnrndisj  34583  reprsuc  34593  breprexplema  34608  bnj918  34743  bnj95  34841  bnj1489  35033  fineqvac  35074  subfacp1lem5  35152  erdszelem5  35163  erdszelem8  35166  cvmliftlem4  35256  cvmliftlem5  35257  cvmlift2lem6  35276  cvmlift2lem9  35279  cvmlift2lem12  35282  satfv1lem  35330  prv1n  35399  brapply  35902  brsuccf  35905  altopthsn  35925  hfsn  36143  neibastop2lem  36324  topjoin  36329  onpsstopbas  36394  weiunse  36432  bj-2uplex  36986  bj-restsn  37046  finixpnum  37575  ptrest  37589  poimirlem3  37593  poimirlem4  37594  poimirlem28  37618  fdc  37715  heiborlem8  37788  ismrer1  37808  grposnOLD  37852  zrdivrng  37923  ecexALTV  38295  eccnvepex  38299  ldualset  39089  lineset  39703  dvaset  40970  dvhset  41046  dibval  41107  dibfna  41119  sticksstones9  42113  frlmsnic  42510  evlsvvval  42533  evlsevl  42541  elrfi  42664  wopprc  43001  dfac11  43033  kelac2  43036  safesnsupfidom1o  43388  sn1dom  43497  pr2dom  43498  tr3dom  43499  fvilbdRP  43661  brtrclfv2  43698  frege110  43944  frege133  43967  k0004lem3  44120  mnuprdlem1  44244  mnuprdlem2  44245  snelpwrVD  44803  fnchoice  45001  elmapsnd  45176  difmapsn  45184  unirnmapsn  45186  ssmapsn  45188  limcresiooub  45619  limcresioolb  45620  cnfdmsn  45859  dvsinax  45890  fourierdlem48  46131  fourierdlem49  46132  sge0sn  46356  sge0p1  46391  ovnovollem1  46633  ovnovollem2  46634  vonvolmbllem  46637  fsetsnf  47028  fsetsnf1  47029  fsetsnfo  47030  cfsetsnfsetfo  47037  setsv  47340  nnsum3primesprm  47752  mapsnop  48267  lindsrng01  48392  snlindsntorlem  48394  snlindsntor  48395  lmod1lem1  48411  lmod1lem2  48412  lmod1lem3  48413  lmod1lem4  48414  lmod1lem5  48415  lmod1  48416  lmod1zr  48417  fv1arycl  48565  1arympt1fv  48567  1arymaptfo  48571  eufsn2  48769  discsubclem  48978  discsubc  48979  iinfconstbas  48981  diag1f1lem  49165  setcsnterm  49323  setc1ocofval  49327  isinito2lem  49331  idfudiag1  49358  diag1f1olem  49366  prstchomval  49384  mndtcbasval  49405  mndtchom  49409  mndtcco  49410  incat  49426  setc1onsubc  49427  aacllem  49613