Theorem snex 5430

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

Syntax hints:  ¬ wn 3   = wceq 1542   ∈ wcel 2107  Vcvv 3475  ∅c0 4321  {csn 4627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3950  df-un 3952  df-nul 4322  df-sn 4628  df-pr 4630

This theorem is referenced by:  prex  5431  snelpwiOLD  5443  intidOLD  5457  elopg  5465  opi1  5467  op1stb  5470  opnz  5472  opeqsng  5502  opeqpr  5504  snopeqop  5505  opthwiener  5513  uniop  5514  0sn0ep  5583  frirr  5652  opthprc  5738  frsn  5761  relop  5848  snsn0non  6486  onnev  6488  onnevOLD  6489  funsneqopb  7145  fsnex  7276  tpex  7729  difsnexi  7743  sucexb  7787  elxp4  7908  elxp5  7909  fvclex  7940  1stval  7972  2ndval  7973  fnse  8114  suppsnop  8158  brtpos2  8212  frrlem13  8278  wfrlem15OLD  8318  tfrlem12  8384  tfrlem16  8388  1oex  8471  naddunif  8688  mapsnd  8876  fvdiagfn  8881  mapsnconst  8882  mapsncnv  8883  mapsnf1o2  8884  ralxpmap  8886  elixpsn  8927  ixpsnf1o  8928  mapsnf1o  8929  ensn1  9013  ensn1OLD  9014  en1bOLD  9020  2dom  9026  mapsnend  9032  snmapen  9034  en2sn  9037  en2snOLD  9038  xpsnen  9051  endisj  9054  xpsnen2g  9061  domunsncan  9068  enfixsn  9077  disjenex  9131  domssex2  9133  domssex  9134  map2xp  9143  pssnn  9164  phplem2OLD  9214  snnen2o  9233  isinf  9256  isinfOLD  9257  pssnnOLD  9261  findcard2OLD  9280  ac6sfi  9283  xpfiOLD  9314  fodomfi  9321  pwfilemOLD  9342  fczfsuppd  9377  snopfsupp  9382  fisn  9418  tc2  9733  tcsni  9734  ranksuc  9856  djuex  9899  fseqenlem1  10015  djuassen  10169  mapdjuen  10171  djudom1  10173  djuinf  10179  ackbij1lem5  10215  cfsuc  10248  dcomex  10438  axdc3lem4  10444  axdc4lem  10446  ttukeylem3  10502  brdom7disj  10522  brdom6disj  10523  fpwwe2lem12  10633  nn0ex  12474  hashxplem  14389  hashf1lem1  14411  hashf1lem1OLD  14412  hashge3el3dif  14443  ofs1  14913  climconst2  15488  ramub1lem2  16956  cshwsex  17030  setsvalg  17095  setsid  17137  pwsbas  17429  pwsle  17434  pwssca  17438  pwssnf1o  17440  imasplusg  17459  imasmulr  17460  imasvsca  17462  imasip  17463  acsfn  17599  homaval  17977  funcsetcestrclem1  18102  mgm1  18573  sgrp1  18616  mnd1  18663  mnd1id  18664  efmnd1bas  18770  idresefmnd  18776  smndex1bas  18783  smndex1sgrp  18785  smndex1mnd  18787  smndex1id  18788  grp1  18926  grp1inv  18927  mulgfval  18946  triv1nsgd  19047  1nsgtrivd  19048  symg2bas  19253  symgvalstructOLD  19258  idrespermg  19272  pmtrsn  19380  psgnsn  19381  abl1  19726  dprdz  19892  dprdsn  19898  simpgnsgd  19962  2nsgsimpgd  19964  ring1  20112  rng1nnzr  20342  pwssplit3  20660  frlmip  21317  islindf4  21377  evlssca  21634  evls1sca  21824  mattposvs  21939  mat1dimelbas  21955  mat1dimscm  21959  mat1dimmul  21960  mat1rhmval  21963  m1detdiag  22081  mdetrlin  22086  mdetrsca2  22088  mdetrlin2  22091  mdetunilem5  22100  smadiadetglem2  22156  basdif0  22438  ordtbas  22678  leordtval2  22698  conncompid  22917  ptbasfi  23067  dfac14lem  23103  dfac14  23104  ptrescn  23125  xkoptsub  23140  pt1hmeo  23292  xpstopnlem1  23295  ufileu  23405  filufint  23406  uffix  23407  uffixsn  23411  flimclslem  23470  ptcmplem1  23538  imasdsf1olem  23861  icccmplem1  24320  icccmplem2  24321  rrxip  24889  rrxsca  24895  ehl1eudis  24919  elply2  25692  plyss  25695  plyeq0lem  25706  taylfval  25853  slerec  27300  0slt1s  27310  ssltleft  27345  ssltright  27346  addsval  27426  addsuniflem  27464  negsid  27495  negsunif  27509  mulsval  27545  ssltmul1  27582  ssltmul2  27583  precsexlem1  27633  precsexlem2  27634  precsexlem11  27643  axlowdimlem15  28194  axlowdim  28199  snstriedgval  28278  vtxvalsnop  28281  iedgvalsnop  28282  upgr1eop  28355  upgr1eopALT  28357  uspgr1eop  28484  usgr1eop  28487  1loopgrvd2  28740  1loopgrvd0  28741  p1evtxdeqlem  28749  p1evtxdeq  28750  p1evtxdp1  28751  uspgrloopvtx  28752  uspgrloopiedg  28754  uspgrloopedg  28755  wlkp1lem4  28913  0pthonv  29362  eupth2lem3  29469  wlkl0  29600  0ofval  30018  suppovss  31884  resf1o  31933  elrspunsn  32505  drngidlhash  32510  zar0ring  32796  ordtconnlem1  32842  esumpr  33002  esumrnmpt2  33004  esumfzf  33005  prsiga  33067  rossros  33116  cntnevol  33164  omsmeas  33260  ccatmulgnn0dir  33491  ofcs1  33493  actfunsnf1o  33554  actfunsnrndisj  33555  reprsuc  33565  breprexplema  33580  bnj918  33715  bnj95  33813  bnj1489  34005  fineqvac  34035  subfacp1lem5  34113  erdszelem5  34124  erdszelem8  34127  cvmliftlem4  34217  cvmliftlem5  34218  cvmlift2lem6  34237  cvmlift2lem9  34240  cvmlift2lem12  34243  satfv1lem  34291  prv1n  34360  brapply  34848  brsuccf  34851  altopthsn  34871  hfsn  35089  gg-cnfldex  35118  neibastop2lem  35183  topjoin  35188  onpsstopbas  35253  bj-2uplex  35841  bj-restsn  35901  finixpnum  36411  ptrest  36425  poimirlem3  36429  poimirlem4  36430  poimirlem28  36454  fdc  36551  heiborlem8  36624  ismrer1  36644  grposnOLD  36688  zrdivrng  36759  ecexALTV  37138  eccnvepex  37142  ldualset  37933  lineset  38547  dvaset  39814  dvhset  39890  dibval  39951  dibfna  39963  sticksstones9  40908  frlmsnic  41060  evlsvvval  41085  evlsevl  41093  elrfi  41365  wopprc  41702  dfac11  41737  kelac2  41740  safesnsupfidom1o  42101  sn1dom  42210  pr2dom  42211  tr3dom  42212  fvilbdRP  42374  brtrclfv2  42411  frege110  42657  frege133  42680  k0004lem3  42833  mnuprdlem1  42964  mnuprdlem2  42965  snelpwrVD  43525  fnchoice  43646  elmapsnd  43836  difmapsn  43844  unirnmapsn  43846  ssmapsn  43848  limcresiooub  44293  limcresioolb  44294  cnfdmsn  44533  dvsinax  44564  fourierdlem48  44805  fourierdlem49  44806  sge0sn  45030  sge0p1  45065  ovnovollem1  45307  ovnovollem2  45308  vonvolmbllem  45311  fsetsnf  45696  fsetsnf1  45697  fsetsnfo  45698  cfsetsnfsetfo  45705  setsv  45981  nnsum3primesprm  46393  mapsnop  46922  lindsrng01  47051  snlindsntorlem  47053  snlindsntor  47054  lmod1lem1  47070  lmod1lem2  47071  lmod1lem3  47072  lmod1lem4  47073  lmod1lem5  47074  lmod1  47075  lmod1zr  47076  fv1arycl  47225  1arympt1fv  47227  1arymaptfo  47231  eufsn2  47411  prstchomval  47596  mndtcbasval  47608  mndtchom  47612  mndtcco  47613  aacllem  47750