Theorem snex 5378

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

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2113  Vcvv 3437  ∅c0 4282  {csn 4577

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901  df-un 3903  df-nul 4283  df-sn 4578  df-pr 4580

This theorem is referenced by:  prex  5379  elopg  5411  opi1  5413  op1stb  5416  opnz  5418  opeqsng  5448  opeqpr  5450  snopeqop  5451  opthwiener  5459  uniop  5460  0sn0ep  5525  frirr  5597  opthprc  5685  frsn  5709  relop  5796  snsn0non  6440  onnev  6442  funsneqopb  7094  fsnex  7226  tpex  7688  difsnexi  7703  sucexb  7746  elxp4  7861  elxp5  7862  fvclex  7900  1stval  7932  2ndval  7933  fnse  8072  suppsnop  8117  brtpos2  8171  frrlem13  8237  tfrlem12  8317  tfrlem16  8321  1oex  8404  naddunif  8617  mapsnd  8820  fvdiagfn  8825  mapsnconst  8826  mapsncnv  8827  mapsnf1o2  8828  ralxpmap  8830  elixpsn  8871  ixpsnf1o  8872  mapsnf1o  8873  ensn1  8954  2dom  8963  mapsnend  8969  snmapen  8971  en2sn  8974  xpsnen  8985  endisj  8988  xpsnen2g  8994  domunsncan  9001  enfixsn  9010  disjenex  9059  domssex2  9061  domssex  9062  map2xp  9071  pssnn  9089  snnen2o  9140  isinf  9160  ac6sfi  9179  fodomfiOLD  9225  fczfsuppd  9281  snopfsupp  9286  fisn  9322  tc2  9641  tcsni  9642  ranksuc  9769  djuex  9812  fseqenlem1  9926  djuassen  10081  mapdjuen  10083  djudom1  10085  djuinf  10091  ackbij1lem5  10125  cfsuc  10159  dcomex  10349  axdc3lem4  10355  axdc4lem  10357  ttukeylem3  10413  brdom7disj  10433  brdom6disj  10434  fpwwe2lem12  10544  nn0ex  12398  hashxplem  14347  hashf1lem1  14369  hashge3el3dif  14401  ofs1  14884  climconst2  15462  ramub1lem2  16946  cshwsex  17019  setsvalg  17084  setsid  17125  pwsbas  17398  pwsle  17404  pwssca  17408  pwssnf1o  17410  imasplusg  17429  imasmulr  17430  imasvsca  17432  imasip  17433  acsfn  17573  homaval  17946  funcsetcestrclem1  18068  mgm1  18574  sgrp1  18645  mnd1  18695  mnd1id  18696  efmnd1bas  18809  idresefmnd  18815  smndex1bas  18822  smndex1sgrp  18824  smndex1mnd  18826  smndex1id  18827  grp1  18968  grp1inv  18969  mulgfval  18990  triv1nsgd  19093  1nsgtrivd  19094  symg2bas  19313  idrespermg  19331  pmtrsn  19439  psgnsn  19440  abl1  19786  dprdz  19952  dprdsn  19958  simpgnsgd  20022  2nsgsimpgd  20024  ring1  20236  rng1nnzr  20699  pwssplit3  21004  cnfldex  21303  pzriprnglem13  21439  pzriprnglem14  21440  frlmip  21724  islindf4  21784  evlsvvval  22039  evlssca  22040  psdmul  22100  evls1sca  22258  mattposvs  22390  mat1dimelbas  22406  mat1dimscm  22410  mat1dimmul  22411  mat1rhmval  22414  m1detdiag  22532  mdetrlin  22537  mdetrsca2  22539  mdetrlin2  22542  mdetunilem5  22551  smadiadetglem2  22607  basdif0  22888  ordtbas  23127  leordtval2  23147  conncompid  23366  ptbasfi  23516  dfac14lem  23552  dfac14  23553  ptrescn  23574  xkoptsub  23589  pt1hmeo  23741  xpstopnlem1  23744  ufileu  23854  filufint  23855  uffix  23856  uffixsn  23860  flimclslem  23919  ptcmplem1  23987  imasdsf1olem  24308  icccmplem1  24758  icccmplem2  24759  rrxip  25337  rrxsca  25343  ehl1eudis  25367  elply2  26148  plyss  26151  plyeq0lem  26162  taylfval  26313  ssltsnb  27752  slerec  27780  eqscut3  27785  0slt1s  27793  ssltleft  27835  ssltright  27836  addsval  27925  addsuniflem  27964  negsid  28003  negsunif  28017  mulsval  28068  ssltmul1  28106  ssltmul2  28107  precsexlem1  28165  precsexlem2  28166  precsexlem11  28175  n0sfincut  28302  0reno  28419  axlowdimlem15  28955  axlowdim  28960  snstriedgval  29037  vtxvalsnop  29040  iedgvalsnop  29041  upgr1eop  29114  upgr1eopALT  29116  uspgr1eop  29246  usgr1eop  29249  1loopgrvd2  29503  1loopgrvd0  29504  p1evtxdeqlem  29512  p1evtxdeq  29513  p1evtxdp1  29514  uspgrloopvtx  29515  uspgrloopiedg  29517  uspgrloopedg  29518  wlkp1lem4  29674  0pthonv  30130  eupth2lem3  30237  wlkl0  30368  0ofval  30788  suppovss  32686  resf1o  32737  elrgspnlem4  33255  elrspunsn  33438  drngidlhash  33443  zar0ring  33963  ordtconnlem1  34009  esumpr  34151  esumrnmpt2  34153  esumfzf  34154  prsiga  34216  rossros  34265  cntnevol  34313  omsmeas  34408  ccatmulgnn0dir  34627  ofcs1  34629  actfunsnf1o  34689  actfunsnrndisj  34690  reprsuc  34700  breprexplema  34715  bnj918  34850  bnj95  34948  bnj1489  35140  fineqvac  35211  subfacp1lem5  35300  erdszelem5  35311  erdszelem8  35314  cvmliftlem4  35404  cvmliftlem5  35405  cvmlift2lem6  35424  cvmlift2lem9  35427  cvmlift2lem12  35430  satfv1lem  35478  prv1n  35547  brapply  36052  lemsuccf  36055  altopthsn  36077  hfsn  36295  neibastop2lem  36476  topjoin  36481  onpsstopbas  36546  weiunse  36584  bj-2uplex  37139  bj-restsn  37199  finixpnum  37718  ptrest  37732  poimirlem3  37736  poimirlem4  37737  poimirlem28  37761  fdc  37858  heiborlem8  37931  ismrer1  37951  grposnOLD  37995  zrdivrng  38066  ldualset  39297  lineset  39910  dvaset  41177  dvhset  41253  dibval  41314  dibfna  41326  sticksstones9  42320  frlmsnic  42710  evlsevl  42732  elrfi  42851  wopprc  43187  dfac11  43219  kelac2  43222  safesnsupfidom1o  43574  sn1dom  43683  pr2dom  43684  tr3dom  43685  fvilbdRP  43847  brtrclfv2  43884  frege110  44130  frege133  44153  k0004lem3  44306  mnuprdlem1  44429  mnuprdlem2  44430  snelpwrVD  44987  nregmodelf1o  45172  fnchoice  45190  elmapsnd  45364  difmapsn  45372  unirnmapsn  45374  ssmapsn  45376  limcresiooub  45802  limcresioolb  45803  cnfdmsn  46042  dvsinax  46073  fourierdlem48  46314  fourierdlem49  46315  sge0sn  46539  sge0p1  46574  ovnovollem1  46816  ovnovollem2  46817  vonvolmbllem  46820  nthrucw  47046  fsetsnf  47213  fsetsnf1  47214  fsetsnfo  47215  cfsetsnfsetfo  47222  setsv  47540  nnsum3primesprm  47952  mapsnop  48506  lindsrng01  48630  snlindsntorlem  48632  snlindsntor  48633  lmod1lem1  48649  lmod1lem2  48650  lmod1lem3  48651  lmod1lem4  48652  lmod1lem5  48653  lmod1  48654  lmod1zr  48655  fv1arycl  48799  1arympt1fv  48801  1arymaptfo  48805  eufsn2  49004  discsubclem  49224  discsubc  49225  iinfconstbas  49227  diag1f1lem  49467  setcsnterm  49651  setc1ocofval  49655  isinito2lem  49659  idfudiag1  49686  diag1f1olem  49694  prstchomval  49720  mndtcbasval  49741  mndtchom  49745  mndtcco  49746  incat  49762  setc1onsubc  49763  aacllem  49962