Theorem snex 5386

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

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2109  Vcvv 3444  ∅c0 4292  {csn 4585

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914  df-un 3916  df-nul 4293  df-sn 4586  df-pr 4588

This theorem is referenced by:  prex  5387  snelpwiOLD  5399  intidOLD  5413  elopg  5421  opi1  5423  op1stb  5426  opnz  5428  opeqsng  5458  opeqpr  5460  snopeqop  5461  opthwiener  5469  uniop  5470  0sn0ep  5535  frirr  5607  opthprc  5695  frsn  5719  relop  5804  snsn0non  6447  onnev  6449  funsneqopb  7106  fsnex  7240  tpex  7702  difsnexi  7717  sucexb  7760  elxp4  7878  elxp5  7879  fvclex  7917  1stval  7949  2ndval  7950  fnse  8089  suppsnop  8134  brtpos2  8188  frrlem13  8254  tfrlem12  8334  tfrlem16  8338  1oex  8421  naddunif  8634  mapsnd  8836  fvdiagfn  8841  mapsnconst  8842  mapsncnv  8843  mapsnf1o2  8844  ralxpmap  8846  elixpsn  8887  ixpsnf1o  8888  mapsnf1o  8889  ensn1  8969  2dom  8978  mapsnend  8984  snmapen  8986  en2sn  8989  xpsnen  9002  endisj  9005  xpsnen2g  9011  domunsncan  9018  enfixsn  9027  disjenex  9076  domssex2  9078  domssex  9079  map2xp  9088  pssnn  9109  snnen2o  9161  isinf  9183  isinfOLD  9184  ac6sfi  9207  xpfiOLD  9246  fodomfiOLD  9257  fczfsuppd  9313  snopfsupp  9318  fisn  9354  tc2  9671  tcsni  9672  ranksuc  9794  djuex  9837  fseqenlem1  9953  djuassen  10108  mapdjuen  10110  djudom1  10112  djuinf  10118  ackbij1lem5  10152  cfsuc  10186  dcomex  10376  axdc3lem4  10382  axdc4lem  10384  ttukeylem3  10440  brdom7disj  10460  brdom6disj  10461  fpwwe2lem12  10571  nn0ex  12424  hashxplem  14374  hashf1lem1  14396  hashge3el3dif  14428  ofs1  14912  climconst2  15490  ramub1lem2  16974  cshwsex  17047  setsvalg  17112  setsid  17153  pwsbas  17426  pwsle  17431  pwssca  17435  pwssnf1o  17437  imasplusg  17456  imasmulr  17457  imasvsca  17459  imasip  17460  acsfn  17596  homaval  17969  funcsetcestrclem1  18091  mgm1  18561  sgrp1  18632  mnd1  18682  mnd1id  18683  efmnd1bas  18796  idresefmnd  18802  smndex1bas  18809  smndex1sgrp  18811  smndex1mnd  18813  smndex1id  18814  grp1  18955  grp1inv  18956  mulgfval  18977  triv1nsgd  19081  1nsgtrivd  19082  symg2bas  19299  idrespermg  19317  pmtrsn  19425  psgnsn  19426  abl1  19772  dprdz  19938  dprdsn  19944  simpgnsgd  20008  2nsgsimpgd  20010  ring1  20195  rng1nnzr  20660  pwssplit3  20944  cnfldex  21243  pzriprnglem13  21379  pzriprnglem14  21380  frlmip  21663  islindf4  21723  evlssca  21972  psdmul  22029  evls1sca  22186  mattposvs  22318  mat1dimelbas  22334  mat1dimscm  22338  mat1dimmul  22339  mat1rhmval  22342  m1detdiag  22460  mdetrlin  22465  mdetrsca2  22467  mdetrlin2  22470  mdetunilem5  22479  smadiadetglem2  22535  basdif0  22816  ordtbas  23055  leordtval2  23075  conncompid  23294  ptbasfi  23444  dfac14lem  23480  dfac14  23481  ptrescn  23502  xkoptsub  23517  pt1hmeo  23669  xpstopnlem1  23672  ufileu  23782  filufint  23783  uffix  23784  uffixsn  23788  flimclslem  23847  ptcmplem1  23915  imasdsf1olem  24237  icccmplem1  24687  icccmplem2  24688  rrxip  25266  rrxsca  25272  ehl1eudis  25296  elply2  26077  plyss  26080  plyeq0lem  26091  taylfval  26242  ssltsn  27680  slerec  27707  0slt1s  27717  ssltleft  27758  ssltright  27759  addsval  27845  addsuniflem  27884  negsid  27923  negsunif  27937  mulsval  27988  ssltmul1  28026  ssltmul2  28027  precsexlem1  28085  precsexlem2  28086  precsexlem11  28095  n0sfincut  28222  0reno  28324  axlowdimlem15  28859  axlowdim  28864  snstriedgval  28941  vtxvalsnop  28944  iedgvalsnop  28945  upgr1eop  29018  upgr1eopALT  29020  uspgr1eop  29150  usgr1eop  29153  1loopgrvd2  29407  1loopgrvd0  29408  p1evtxdeqlem  29416  p1evtxdeq  29417  p1evtxdp1  29418  uspgrloopvtx  29419  uspgrloopiedg  29421  uspgrloopedg  29422  wlkp1lem4  29578  0pthonv  30031  eupth2lem3  30138  wlkl0  30269  0ofval  30689  suppovss  32577  resf1o  32626  elrgspnlem4  33169  elrspunsn  33373  drngidlhash  33378  zar0ring  33841  ordtconnlem1  33887  esumpr  34029  esumrnmpt2  34031  esumfzf  34032  prsiga  34094  rossros  34143  cntnevol  34191  omsmeas  34287  ccatmulgnn0dir  34506  ofcs1  34508  actfunsnf1o  34568  actfunsnrndisj  34569  reprsuc  34579  breprexplema  34594  bnj918  34729  bnj95  34827  bnj1489  35019  fineqvac  35060  subfacp1lem5  35144  erdszelem5  35155  erdszelem8  35158  cvmliftlem4  35248  cvmliftlem5  35249  cvmlift2lem6  35268  cvmlift2lem9  35271  cvmlift2lem12  35274  satfv1lem  35322  prv1n  35391  brapply  35899  brsuccf  35902  altopthsn  35922  hfsn  36140  neibastop2lem  36321  topjoin  36326  onpsstopbas  36391  weiunse  36429  bj-2uplex  36983  bj-restsn  37043  finixpnum  37572  ptrest  37586  poimirlem3  37590  poimirlem4  37591  poimirlem28  37615  fdc  37712  heiborlem8  37785  ismrer1  37805  grposnOLD  37849  zrdivrng  37920  ldualset  39091  lineset  39705  dvaset  40972  dvhset  41048  dibval  41109  dibfna  41121  sticksstones9  42115  frlmsnic  42501  evlsvvval  42524  evlsevl  42532  elrfi  42655  wopprc  42992  dfac11  43024  kelac2  43027  safesnsupfidom1o  43379  sn1dom  43488  pr2dom  43489  tr3dom  43490  fvilbdRP  43652  brtrclfv2  43689  frege110  43935  frege133  43958  k0004lem3  44111  mnuprdlem1  44234  mnuprdlem2  44235  snelpwrVD  44793  nregmodelf1o  44978  fnchoice  44996  elmapsnd  45171  difmapsn  45179  unirnmapsn  45181  ssmapsn  45183  limcresiooub  45613  limcresioolb  45614  cnfdmsn  45853  dvsinax  45884  fourierdlem48  46125  fourierdlem49  46126  sge0sn  46350  sge0p1  46385  ovnovollem1  46627  ovnovollem2  46628  vonvolmbllem  46631  fsetsnf  47025  fsetsnf1  47026  fsetsnfo  47027  cfsetsnfsetfo  47034  setsv  47352  nnsum3primesprm  47764  mapsnop  48305  lindsrng01  48430  snlindsntorlem  48432  snlindsntor  48433  lmod1lem1  48449  lmod1lem2  48450  lmod1lem3  48451  lmod1lem4  48452  lmod1lem5  48453  lmod1  48454  lmod1zr  48455  fv1arycl  48599  1arympt1fv  48601  1arymaptfo  48605  eufsn2  48804  discsubclem  49025  discsubc  49026  iinfconstbas  49028  diag1f1lem  49268  setcsnterm  49452  setc1ocofval  49456  isinito2lem  49460  idfudiag1  49487  diag1f1olem  49495  prstchomval  49521  mndtcbasval  49542  mndtchom  49546  mndtcco  49547  incat  49563  setc1onsubc  49564  aacllem  49763