Theorem snex 5431

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

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2105  Vcvv 3473  ∅c0 4322  {csn 4628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-dif 3951  df-un 3953  df-nul 4323  df-sn 4629  df-pr 4631

This theorem is referenced by:  prex  5432  snelpwiOLD  5444  intidOLD  5458  elopg  5466  opi1  5468  op1stb  5471  opnz  5473  opeqsng  5503  opeqpr  5505  snopeqop  5506  opthwiener  5514  uniop  5515  0sn0ep  5584  frirr  5653  opthprc  5740  frsn  5763  relop  5850  snsn0non  6489  onnev  6491  onnevOLD  6492  funsneqopb  7152  fsnex  7284  tpex  7738  difsnexi  7752  sucexb  7796  elxp4  7917  elxp5  7918  fvclex  7949  1stval  7981  2ndval  7982  fnse  8124  suppsnop  8168  brtpos2  8223  frrlem13  8289  wfrlem15OLD  8329  tfrlem12  8395  tfrlem16  8399  1oex  8482  naddunif  8698  mapsnd  8886  fvdiagfn  8891  mapsnconst  8892  mapsncnv  8893  mapsnf1o2  8894  ralxpmap  8896  elixpsn  8937  ixpsnf1o  8938  mapsnf1o  8939  ensn1  9023  ensn1OLD  9024  en1bOLD  9030  2dom  9036  mapsnend  9042  snmapen  9044  en2sn  9047  en2snOLD  9048  xpsnen  9061  endisj  9064  xpsnen2g  9071  domunsncan  9078  enfixsn  9087  disjenex  9141  domssex2  9143  domssex  9144  map2xp  9153  pssnn  9174  phplem2OLD  9224  snnen2o  9243  isinf  9266  isinfOLD  9267  pssnnOLD  9271  findcard2OLD  9290  ac6sfi  9293  xpfiOLD  9324  fodomfi  9331  pwfilemOLD  9352  fczfsuppd  9387  snopfsupp  9392  fisn  9428  tc2  9743  tcsni  9744  ranksuc  9866  djuex  9909  fseqenlem1  10025  djuassen  10179  mapdjuen  10181  djudom1  10183  djuinf  10189  ackbij1lem5  10225  cfsuc  10258  dcomex  10448  axdc3lem4  10454  axdc4lem  10456  ttukeylem3  10512  brdom7disj  10532  brdom6disj  10533  fpwwe2lem12  10643  nn0ex  12485  hashxplem  14400  hashf1lem1  14422  hashf1lem1OLD  14423  hashge3el3dif  14454  ofs1  14924  climconst2  15499  ramub1lem2  16967  cshwsex  17041  setsvalg  17106  setsid  17148  pwsbas  17440  pwsle  17445  pwssca  17449  pwssnf1o  17451  imasplusg  17470  imasmulr  17471  imasvsca  17473  imasip  17474  acsfn  17610  homaval  17991  funcsetcestrclem1  18116  mgm1  18589  sgrp1  18660  mnd1  18707  mnd1id  18708  efmnd1bas  18816  idresefmnd  18822  smndex1bas  18829  smndex1sgrp  18831  smndex1mnd  18833  smndex1id  18834  grp1  18973  grp1inv  18974  mulgfval  18995  triv1nsgd  19096  1nsgtrivd  19097  symg2bas  19308  symgvalstructOLD  19313  idrespermg  19327  pmtrsn  19435  psgnsn  19436  abl1  19782  dprdz  19948  dprdsn  19954  simpgnsgd  20018  2nsgsimpgd  20020  ring1  20205  rng1nnzr  20622  pwssplit3  20905  pzriprnglem13  21353  pzriprnglem14  21354  frlmip  21643  islindf4  21703  evlssca  21963  evls1sca  22162  mattposvs  22277  mat1dimelbas  22293  mat1dimscm  22297  mat1dimmul  22298  mat1rhmval  22301  m1detdiag  22419  mdetrlin  22424  mdetrsca2  22426  mdetrlin2  22429  mdetunilem5  22438  smadiadetglem2  22494  basdif0  22776  ordtbas  23016  leordtval2  23036  conncompid  23255  ptbasfi  23405  dfac14lem  23441  dfac14  23442  ptrescn  23463  xkoptsub  23478  pt1hmeo  23630  xpstopnlem1  23633  ufileu  23743  filufint  23744  uffix  23745  uffixsn  23749  flimclslem  23808  ptcmplem1  23876  imasdsf1olem  24199  icccmplem1  24658  icccmplem2  24659  rrxip  25238  rrxsca  25244  ehl1eudis  25268  elply2  26048  plyss  26051  plyeq0lem  26062  taylfval  26210  ssltsn  27638  slerec  27665  0slt1s  27675  ssltleft  27710  ssltright  27711  addsval  27792  addsuniflem  27831  negsid  27866  negsunif  27880  mulsval  27922  ssltmul1  27960  ssltmul2  27961  precsexlem1  28018  precsexlem2  28019  precsexlem11  28028  0reno  28105  axlowdimlem15  28647  axlowdim  28652  snstriedgval  28731  vtxvalsnop  28734  iedgvalsnop  28735  upgr1eop  28808  upgr1eopALT  28810  uspgr1eop  28937  usgr1eop  28940  1loopgrvd2  29193  1loopgrvd0  29194  p1evtxdeqlem  29202  p1evtxdeq  29203  p1evtxdp1  29204  uspgrloopvtx  29205  uspgrloopiedg  29207  uspgrloopedg  29208  wlkp1lem4  29366  0pthonv  29815  eupth2lem3  29922  wlkl0  30053  0ofval  30473  suppovss  32339  resf1o  32388  elrspunsn  32987  drngidlhash  32992  zar0ring  33322  ordtconnlem1  33368  esumpr  33528  esumrnmpt2  33530  esumfzf  33531  prsiga  33593  rossros  33642  cntnevol  33690  omsmeas  33786  ccatmulgnn0dir  34017  ofcs1  34019  actfunsnf1o  34080  actfunsnrndisj  34081  reprsuc  34091  breprexplema  34106  bnj918  34241  bnj95  34339  bnj1489  34531  fineqvac  34561  subfacp1lem5  34639  erdszelem5  34650  erdszelem8  34653  cvmliftlem4  34743  cvmliftlem5  34744  cvmlift2lem6  34763  cvmlift2lem9  34766  cvmlift2lem12  34769  satfv1lem  34817  prv1n  34886  brapply  35380  brsuccf  35383  altopthsn  35403  hfsn  35621  gg-cnfldex  35631  neibastop2lem  35709  topjoin  35714  onpsstopbas  35779  bj-2uplex  36367  bj-restsn  36427  finixpnum  36937  ptrest  36951  poimirlem3  36955  poimirlem4  36956  poimirlem28  36980  fdc  37077  heiborlem8  37150  ismrer1  37170  grposnOLD  37214  zrdivrng  37285  ecexALTV  37664  eccnvepex  37668  ldualset  38459  lineset  39073  dvaset  40340  dvhset  40416  dibval  40477  dibfna  40489  sticksstones9  41437  frlmsnic  41573  evlsvvval  41598  evlsevl  41606  elrfi  41895  wopprc  42232  dfac11  42267  kelac2  42270  safesnsupfidom1o  42631  sn1dom  42740  pr2dom  42741  tr3dom  42742  fvilbdRP  42904  brtrclfv2  42941  frege110  43187  frege133  43210  k0004lem3  43363  mnuprdlem1  43494  mnuprdlem2  43495  snelpwrVD  44055  fnchoice  44176  elmapsnd  44362  difmapsn  44370  unirnmapsn  44372  ssmapsn  44374  limcresiooub  44817  limcresioolb  44818  cnfdmsn  45057  dvsinax  45088  fourierdlem48  45329  fourierdlem49  45330  sge0sn  45554  sge0p1  45589  ovnovollem1  45831  ovnovollem2  45832  vonvolmbllem  45835  fsetsnf  46220  fsetsnf1  46221  fsetsnfo  46222  cfsetsnfsetfo  46229  setsv  46505  nnsum3primesprm  46917  mapsnop  47183  lindsrng01  47311  snlindsntorlem  47313  snlindsntor  47314  lmod1lem1  47330  lmod1lem2  47331  lmod1lem3  47332  lmod1lem4  47333  lmod1lem5  47334  lmod1  47335  lmod1zr  47336  fv1arycl  47485  1arympt1fv  47487  1arymaptfo  47491  eufsn2  47671  prstchomval  47856  mndtcbasval  47868  mndtchom  47872  mndtcco  47873  aacllem  48010