Theorem snex 5441

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

Syntax hints:  ¬ wn 3   = wceq 1536   ∈ wcel 2105  Vcvv 3477  ∅c0 4338  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-un 3967  df-nul 4339  df-sn 4631  df-pr 4633

This theorem is referenced by:  prex  5442  snelpwiOLD  5454  intidOLD  5468  elopg  5476  opi1  5478  op1stb  5481  opnz  5483  opeqsng  5512  opeqpr  5514  snopeqop  5515  opthwiener  5523  uniop  5524  0sn0ep  5592  frirr  5664  opthprc  5752  frsn  5775  relop  5863  snsn0non  6510  onnev  6512  funsneqopb  7171  fsnex  7302  tpex  7764  difsnexi  7779  sucexb  7823  elxp4  7944  elxp5  7945  fvclex  7981  1stval  8014  2ndval  8015  fnse  8156  suppsnop  8201  brtpos2  8255  frrlem13  8321  wfrlem15OLD  8361  tfrlem12  8427  tfrlem16  8431  1oex  8514  naddunif  8729  mapsnd  8924  fvdiagfn  8929  mapsnconst  8930  mapsncnv  8931  mapsnf1o2  8932  ralxpmap  8934  elixpsn  8975  ixpsnf1o  8976  mapsnf1o  8977  ensn1  9059  2dom  9068  mapsnend  9074  snmapen  9076  en2sn  9079  xpsnen  9093  endisj  9096  xpsnen2g  9103  domunsncan  9110  enfixsn  9119  disjenex  9173  domssex2  9175  domssex  9176  map2xp  9185  pssnn  9206  phplem2OLD  9252  snnen2o  9270  isinf  9293  isinfOLD  9294  ac6sfi  9317  xpfiOLD  9356  fodomfiOLD  9367  fczfsuppd  9423  snopfsupp  9428  fisn  9464  tc2  9779  tcsni  9780  ranksuc  9902  djuex  9945  fseqenlem1  10061  djuassen  10216  mapdjuen  10218  djudom1  10220  djuinf  10226  ackbij1lem5  10260  cfsuc  10294  dcomex  10484  axdc3lem4  10490  axdc4lem  10492  ttukeylem3  10548  brdom7disj  10568  brdom6disj  10569  fpwwe2lem12  10679  nn0ex  12529  hashxplem  14468  hashf1lem1  14490  hashge3el3dif  14522  ofs1  15005  climconst2  15580  ramub1lem2  17060  cshwsex  17134  setsvalg  17199  setsid  17241  pwsbas  17533  pwsle  17538  pwssca  17542  pwssnf1o  17544  imasplusg  17563  imasmulr  17564  imasvsca  17566  imasip  17567  acsfn  17703  homaval  18084  funcsetcestrclem1  18209  mgm1  18683  sgrp1  18754  mnd1  18804  mnd1id  18805  efmnd1bas  18918  idresefmnd  18924  smndex1bas  18931  smndex1sgrp  18933  smndex1mnd  18935  smndex1id  18936  grp1  19077  grp1inv  19078  mulgfval  19099  triv1nsgd  19203  1nsgtrivd  19204  symg2bas  19424  symgvalstructOLD  19429  idrespermg  19443  pmtrsn  19551  psgnsn  19552  abl1  19898  dprdz  20064  dprdsn  20070  simpgnsgd  20134  2nsgsimpgd  20136  ring1  20323  rng1nnzr  20792  pwssplit3  21077  cnfldex  21384  pzriprnglem13  21521  pzriprnglem14  21522  frlmip  21815  islindf4  21875  evlssca  22130  psdmul  22187  evls1sca  22342  mattposvs  22476  mat1dimelbas  22492  mat1dimscm  22496  mat1dimmul  22497  mat1rhmval  22500  m1detdiag  22618  mdetrlin  22623  mdetrsca2  22625  mdetrlin2  22628  mdetunilem5  22637  smadiadetglem2  22693  basdif0  22975  ordtbas  23215  leordtval2  23235  conncompid  23454  ptbasfi  23604  dfac14lem  23640  dfac14  23641  ptrescn  23662  xkoptsub  23677  pt1hmeo  23829  xpstopnlem1  23832  ufileu  23942  filufint  23943  uffix  23944  uffixsn  23948  flimclslem  24007  ptcmplem1  24075  imasdsf1olem  24398  icccmplem1  24857  icccmplem2  24858  rrxip  25437  rrxsca  25443  ehl1eudis  25467  elply2  26249  plyss  26252  plyeq0lem  26263  taylfval  26414  ssltsn  27851  slerec  27878  0slt1s  27888  ssltleft  27923  ssltright  27924  addsval  28009  addsuniflem  28048  negsid  28087  negsunif  28101  mulsval  28149  ssltmul1  28187  ssltmul2  28188  precsexlem1  28245  precsexlem2  28246  precsexlem11  28255  nohalf  28421  0reno  28443  axlowdimlem15  28985  axlowdim  28990  snstriedgval  29069  vtxvalsnop  29072  iedgvalsnop  29073  upgr1eop  29146  upgr1eopALT  29148  uspgr1eop  29278  usgr1eop  29281  1loopgrvd2  29535  1loopgrvd0  29536  p1evtxdeqlem  29544  p1evtxdeq  29545  p1evtxdp1  29546  uspgrloopvtx  29547  uspgrloopiedg  29549  uspgrloopedg  29550  wlkp1lem4  29708  0pthonv  30157  eupth2lem3  30264  wlkl0  30395  0ofval  30815  suppovss  32695  resf1o  32747  elrgspnlem4  33234  elrspunsn  33436  drngidlhash  33441  zar0ring  33838  ordtconnlem1  33884  esumpr  34046  esumrnmpt2  34048  esumfzf  34049  prsiga  34111  rossros  34160  cntnevol  34208  omsmeas  34304  ccatmulgnn0dir  34535  ofcs1  34537  actfunsnf1o  34597  actfunsnrndisj  34598  reprsuc  34608  breprexplema  34623  bnj918  34758  bnj95  34856  bnj1489  35048  fineqvac  35089  subfacp1lem5  35168  erdszelem5  35179  erdszelem8  35182  cvmliftlem4  35272  cvmliftlem5  35273  cvmlift2lem6  35292  cvmlift2lem9  35295  cvmlift2lem12  35298  satfv1lem  35346  prv1n  35415  brapply  35919  brsuccf  35922  altopthsn  35942  hfsn  36160  neibastop2lem  36342  topjoin  36347  onpsstopbas  36412  weiunse  36450  bj-2uplex  37004  bj-restsn  37064  finixpnum  37591  ptrest  37605  poimirlem3  37609  poimirlem4  37610  poimirlem28  37634  fdc  37731  heiborlem8  37804  ismrer1  37824  grposnOLD  37868  zrdivrng  37939  ecexALTV  38312  eccnvepex  38316  ldualset  39106  lineset  39720  dvaset  40987  dvhset  41063  dibval  41124  dibfna  41136  sticksstones9  42135  frlmsnic  42526  evlsvvval  42549  evlsevl  42557  elrfi  42681  wopprc  43018  dfac11  43050  kelac2  43053  safesnsupfidom1o  43406  sn1dom  43515  pr2dom  43516  tr3dom  43517  fvilbdRP  43679  brtrclfv2  43716  frege110  43962  frege133  43985  k0004lem3  44138  mnuprdlem1  44267  mnuprdlem2  44268  snelpwrVD  44828  fnchoice  44966  elmapsnd  45146  difmapsn  45154  unirnmapsn  45156  ssmapsn  45158  limcresiooub  45597  limcresioolb  45598  cnfdmsn  45837  dvsinax  45868  fourierdlem48  46109  fourierdlem49  46110  sge0sn  46334  sge0p1  46369  ovnovollem1  46611  ovnovollem2  46612  vonvolmbllem  46615  fsetsnf  47000  fsetsnf1  47001  fsetsnfo  47002  cfsetsnfsetfo  47009  setsv  47302  nnsum3primesprm  47714  mapsnop  48188  lindsrng01  48313  snlindsntorlem  48315  snlindsntor  48316  lmod1lem1  48332  lmod1lem2  48333  lmod1lem3  48334  lmod1lem4  48335  lmod1lem5  48336  lmod1  48337  lmod1zr  48338  fv1arycl  48486  1arympt1fv  48488  1arymaptfo  48492  eufsn2  48672  prstchomval  48874  mndtcbasval  48888  mndtchom  48892  mndtcco  48893  aacllem  49031