Theorem snex 5391

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 5338. (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 5390	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
2		snprc 4681	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
3	2	biimpi 216	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴} = ∅)
4		0ex 5262	. . 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 3447  ∅c0 4296  {csn 4589

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 5251  ax-nul 5261  ax-pr 5387

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 3449  df-dif 3917  df-un 3919  df-nul 4297  df-sn 4590  df-pr 4592

This theorem is referenced by:  prex  5392  snelpwiOLD  5404  intidOLD  5418  elopg  5426  opi1  5428  op1stb  5431  opnz  5433  opeqsng  5463  opeqpr  5465  snopeqop  5466  opthwiener  5474  uniop  5475  0sn0ep  5542  frirr  5614  opthprc  5702  frsn  5726  relop  5814  snsn0non  6459  onnev  6461  funsneqopb  7124  fsnex  7258  tpex  7722  difsnexi  7737  sucexb  7780  elxp4  7898  elxp5  7899  fvclex  7937  1stval  7970  2ndval  7971  fnse  8112  suppsnop  8157  brtpos2  8211  frrlem13  8277  tfrlem12  8357  tfrlem16  8361  1oex  8444  naddunif  8657  mapsnd  8859  fvdiagfn  8864  mapsnconst  8865  mapsncnv  8866  mapsnf1o2  8867  ralxpmap  8869  elixpsn  8910  ixpsnf1o  8911  mapsnf1o  8912  ensn1  8992  2dom  9001  mapsnend  9007  snmapen  9009  en2sn  9012  xpsnen  9025  endisj  9028  xpsnen2g  9034  domunsncan  9041  enfixsn  9050  disjenex  9099  domssex2  9101  domssex  9102  map2xp  9111  pssnn  9132  snnen2o  9184  isinf  9207  isinfOLD  9208  ac6sfi  9231  xpfiOLD  9270  fodomfiOLD  9281  fczfsuppd  9337  snopfsupp  9342  fisn  9378  tc2  9695  tcsni  9696  ranksuc  9818  djuex  9861  fseqenlem1  9977  djuassen  10132  mapdjuen  10134  djudom1  10136  djuinf  10142  ackbij1lem5  10176  cfsuc  10210  dcomex  10400  axdc3lem4  10406  axdc4lem  10408  ttukeylem3  10464  brdom7disj  10484  brdom6disj  10485  fpwwe2lem12  10595  nn0ex  12448  hashxplem  14398  hashf1lem1  14420  hashge3el3dif  14452  ofs1  14936  climconst2  15514  ramub1lem2  16998  cshwsex  17071  setsvalg  17136  setsid  17177  pwsbas  17450  pwsle  17455  pwssca  17459  pwssnf1o  17461  imasplusg  17480  imasmulr  17481  imasvsca  17483  imasip  17484  acsfn  17620  homaval  17993  funcsetcestrclem1  18115  mgm1  18585  sgrp1  18656  mnd1  18706  mnd1id  18707  efmnd1bas  18820  idresefmnd  18826  smndex1bas  18833  smndex1sgrp  18835  smndex1mnd  18837  smndex1id  18838  grp1  18979  grp1inv  18980  mulgfval  19001  triv1nsgd  19105  1nsgtrivd  19106  symg2bas  19323  idrespermg  19341  pmtrsn  19449  psgnsn  19450  abl1  19796  dprdz  19962  dprdsn  19968  simpgnsgd  20032  2nsgsimpgd  20034  ring1  20219  rng1nnzr  20684  pwssplit3  20968  cnfldex  21267  pzriprnglem13  21403  pzriprnglem14  21404  frlmip  21687  islindf4  21747  evlssca  21996  psdmul  22053  evls1sca  22210  mattposvs  22342  mat1dimelbas  22358  mat1dimscm  22362  mat1dimmul  22363  mat1rhmval  22366  m1detdiag  22484  mdetrlin  22489  mdetrsca2  22491  mdetrlin2  22494  mdetunilem5  22503  smadiadetglem2  22559  basdif0  22840  ordtbas  23079  leordtval2  23099  conncompid  23318  ptbasfi  23468  dfac14lem  23504  dfac14  23505  ptrescn  23526  xkoptsub  23541  pt1hmeo  23693  xpstopnlem1  23696  ufileu  23806  filufint  23807  uffix  23808  uffixsn  23812  flimclslem  23871  ptcmplem1  23939  imasdsf1olem  24261  icccmplem1  24711  icccmplem2  24712  rrxip  25290  rrxsca  25296  ehl1eudis  25320  elply2  26101  plyss  26104  plyeq0lem  26115  taylfval  26266  ssltsn  27704  slerec  27731  0slt1s  27741  ssltleft  27782  ssltright  27783  addsval  27869  addsuniflem  27908  negsid  27947  negsunif  27961  mulsval  28012  ssltmul1  28050  ssltmul2  28051  precsexlem1  28109  precsexlem2  28110  precsexlem11  28119  n0sfincut  28246  0reno  28348  axlowdimlem15  28883  axlowdim  28888  snstriedgval  28965  vtxvalsnop  28968  iedgvalsnop  28969  upgr1eop  29042  upgr1eopALT  29044  uspgr1eop  29174  usgr1eop  29177  1loopgrvd2  29431  1loopgrvd0  29432  p1evtxdeqlem  29440  p1evtxdeq  29441  p1evtxdp1  29442  uspgrloopvtx  29443  uspgrloopiedg  29445  uspgrloopedg  29446  wlkp1lem4  29604  0pthonv  30058  eupth2lem3  30165  wlkl0  30296  0ofval  30716  suppovss  32604  resf1o  32653  elrgspnlem4  33196  elrspunsn  33400  drngidlhash  33405  zar0ring  33868  ordtconnlem1  33914  esumpr  34056  esumrnmpt2  34058  esumfzf  34059  prsiga  34121  rossros  34170  cntnevol  34218  omsmeas  34314  ccatmulgnn0dir  34533  ofcs1  34535  actfunsnf1o  34595  actfunsnrndisj  34596  reprsuc  34606  breprexplema  34621  bnj918  34756  bnj95  34854  bnj1489  35046  fineqvac  35087  subfacp1lem5  35171  erdszelem5  35182  erdszelem8  35185  cvmliftlem4  35275  cvmliftlem5  35276  cvmlift2lem6  35295  cvmlift2lem9  35298  cvmlift2lem12  35301  satfv1lem  35349  prv1n  35418  brapply  35926  brsuccf  35929  altopthsn  35949  hfsn  36167  neibastop2lem  36348  topjoin  36353  onpsstopbas  36418  weiunse  36456  bj-2uplex  37010  bj-restsn  37070  finixpnum  37599  ptrest  37613  poimirlem3  37617  poimirlem4  37618  poimirlem28  37642  fdc  37739  heiborlem8  37812  ismrer1  37832  grposnOLD  37876  zrdivrng  37947  ldualset  39118  lineset  39732  dvaset  40999  dvhset  41075  dibval  41136  dibfna  41148  sticksstones9  42142  frlmsnic  42528  evlsvvval  42551  evlsevl  42559  elrfi  42682  wopprc  43019  dfac11  43051  kelac2  43054  safesnsupfidom1o  43406  sn1dom  43515  pr2dom  43516  tr3dom  43517  fvilbdRP  43679  brtrclfv2  43716  frege110  43962  frege133  43985  k0004lem3  44138  mnuprdlem1  44261  mnuprdlem2  44262  snelpwrVD  44820  nregmodelf1o  45005  fnchoice  45023  elmapsnd  45198  difmapsn  45206  unirnmapsn  45208  ssmapsn  45210  limcresiooub  45640  limcresioolb  45641  cnfdmsn  45880  dvsinax  45911  fourierdlem48  46152  fourierdlem49  46153  sge0sn  46377  sge0p1  46412  ovnovollem1  46654  ovnovollem2  46655  vonvolmbllem  46658  fsetsnf  47052  fsetsnf1  47053  fsetsnfo  47054  cfsetsnfsetfo  47061  setsv  47379  nnsum3primesprm  47791  mapsnop  48332  lindsrng01  48457  snlindsntorlem  48459  snlindsntor  48460  lmod1lem1  48476  lmod1lem2  48477  lmod1lem3  48478  lmod1lem4  48479  lmod1lem5  48480  lmod1  48481  lmod1zr  48482  fv1arycl  48626  1arympt1fv  48628  1arymaptfo  48632  eufsn2  48831  discsubclem  49052  discsubc  49053  iinfconstbas  49055  diag1f1lem  49295  setcsnterm  49479  setc1ocofval  49483  isinito2lem  49487  idfudiag1  49514  diag1f1olem  49522  prstchomval  49548  mndtcbasval  49569  mndtchom  49573  mndtcco  49574  incat  49590  setc1onsubc  49591  aacllem  49790