Theorem snex 5394

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

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2109  Vcvv 3450  ∅c0 4299  {csn 4592

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-un 3922  df-nul 4300  df-sn 4593  df-pr 4595

This theorem is referenced by:  prex  5395  snelpwiOLD  5407  intidOLD  5421  elopg  5429  opi1  5431  op1stb  5434  opnz  5436  opeqsng  5466  opeqpr  5468  snopeqop  5469  opthwiener  5477  uniop  5478  0sn0ep  5545  frirr  5617  opthprc  5705  frsn  5729  relop  5817  snsn0non  6462  onnev  6464  funsneqopb  7127  fsnex  7261  tpex  7725  difsnexi  7740  sucexb  7783  elxp4  7901  elxp5  7902  fvclex  7940  1stval  7973  2ndval  7974  fnse  8115  suppsnop  8160  brtpos2  8214  frrlem13  8280  tfrlem12  8360  tfrlem16  8364  1oex  8447  naddunif  8660  mapsnd  8862  fvdiagfn  8867  mapsnconst  8868  mapsncnv  8869  mapsnf1o2  8870  ralxpmap  8872  elixpsn  8913  ixpsnf1o  8914  mapsnf1o  8915  ensn1  8995  2dom  9004  mapsnend  9010  snmapen  9012  en2sn  9015  xpsnen  9029  endisj  9032  xpsnen2g  9039  domunsncan  9046  enfixsn  9055  disjenex  9105  domssex2  9107  domssex  9108  map2xp  9117  pssnn  9138  snnen2o  9191  isinf  9214  isinfOLD  9215  ac6sfi  9238  xpfiOLD  9277  fodomfiOLD  9288  fczfsuppd  9344  snopfsupp  9349  fisn  9385  tc2  9702  tcsni  9703  ranksuc  9825  djuex  9868  fseqenlem1  9984  djuassen  10139  mapdjuen  10141  djudom1  10143  djuinf  10149  ackbij1lem5  10183  cfsuc  10217  dcomex  10407  axdc3lem4  10413  axdc4lem  10415  ttukeylem3  10471  brdom7disj  10491  brdom6disj  10492  fpwwe2lem12  10602  nn0ex  12455  hashxplem  14405  hashf1lem1  14427  hashge3el3dif  14459  ofs1  14943  climconst2  15521  ramub1lem2  17005  cshwsex  17078  setsvalg  17143  setsid  17184  pwsbas  17457  pwsle  17462  pwssca  17466  pwssnf1o  17468  imasplusg  17487  imasmulr  17488  imasvsca  17490  imasip  17491  acsfn  17627  homaval  18000  funcsetcestrclem1  18122  mgm1  18592  sgrp1  18663  mnd1  18713  mnd1id  18714  efmnd1bas  18827  idresefmnd  18833  smndex1bas  18840  smndex1sgrp  18842  smndex1mnd  18844  smndex1id  18845  grp1  18986  grp1inv  18987  mulgfval  19008  triv1nsgd  19112  1nsgtrivd  19113  symg2bas  19330  idrespermg  19348  pmtrsn  19456  psgnsn  19457  abl1  19803  dprdz  19969  dprdsn  19975  simpgnsgd  20039  2nsgsimpgd  20041  ring1  20226  rng1nnzr  20691  pwssplit3  20975  cnfldex  21274  pzriprnglem13  21410  pzriprnglem14  21411  frlmip  21694  islindf4  21754  evlssca  22003  psdmul  22060  evls1sca  22217  mattposvs  22349  mat1dimelbas  22365  mat1dimscm  22369  mat1dimmul  22370  mat1rhmval  22373  m1detdiag  22491  mdetrlin  22496  mdetrsca2  22498  mdetrlin2  22501  mdetunilem5  22510  smadiadetglem2  22566  basdif0  22847  ordtbas  23086  leordtval2  23106  conncompid  23325  ptbasfi  23475  dfac14lem  23511  dfac14  23512  ptrescn  23533  xkoptsub  23548  pt1hmeo  23700  xpstopnlem1  23703  ufileu  23813  filufint  23814  uffix  23815  uffixsn  23819  flimclslem  23878  ptcmplem1  23946  imasdsf1olem  24268  icccmplem1  24718  icccmplem2  24719  rrxip  25297  rrxsca  25303  ehl1eudis  25327  elply2  26108  plyss  26111  plyeq0lem  26122  taylfval  26273  ssltsn  27711  slerec  27738  0slt1s  27748  ssltleft  27789  ssltright  27790  addsval  27876  addsuniflem  27915  negsid  27954  negsunif  27968  mulsval  28019  ssltmul1  28057  ssltmul2  28058  precsexlem1  28116  precsexlem2  28117  precsexlem11  28126  n0sfincut  28253  0reno  28355  axlowdimlem15  28890  axlowdim  28895  snstriedgval  28972  vtxvalsnop  28975  iedgvalsnop  28976  upgr1eop  29049  upgr1eopALT  29051  uspgr1eop  29181  usgr1eop  29184  1loopgrvd2  29438  1loopgrvd0  29439  p1evtxdeqlem  29447  p1evtxdeq  29448  p1evtxdp1  29449  uspgrloopvtx  29450  uspgrloopiedg  29452  uspgrloopedg  29453  wlkp1lem4  29611  0pthonv  30065  eupth2lem3  30172  wlkl0  30303  0ofval  30723  suppovss  32611  resf1o  32660  elrgspnlem4  33203  elrspunsn  33407  drngidlhash  33412  zar0ring  33875  ordtconnlem1  33921  esumpr  34063  esumrnmpt2  34065  esumfzf  34066  prsiga  34128  rossros  34177  cntnevol  34225  omsmeas  34321  ccatmulgnn0dir  34540  ofcs1  34542  actfunsnf1o  34602  actfunsnrndisj  34603  reprsuc  34613  breprexplema  34628  bnj918  34763  bnj95  34861  bnj1489  35053  fineqvac  35094  subfacp1lem5  35178  erdszelem5  35189  erdszelem8  35192  cvmliftlem4  35282  cvmliftlem5  35283  cvmlift2lem6  35302  cvmlift2lem9  35305  cvmlift2lem12  35308  satfv1lem  35356  prv1n  35425  brapply  35933  brsuccf  35936  altopthsn  35956  hfsn  36174  neibastop2lem  36355  topjoin  36360  onpsstopbas  36425  weiunse  36463  bj-2uplex  37017  bj-restsn  37077  finixpnum  37606  ptrest  37620  poimirlem3  37624  poimirlem4  37625  poimirlem28  37649  fdc  37746  heiborlem8  37819  ismrer1  37839  grposnOLD  37883  zrdivrng  37954  ldualset  39125  lineset  39739  dvaset  41006  dvhset  41082  dibval  41143  dibfna  41155  sticksstones9  42149  frlmsnic  42535  evlsvvval  42558  evlsevl  42566  elrfi  42689  wopprc  43026  dfac11  43058  kelac2  43061  safesnsupfidom1o  43413  sn1dom  43522  pr2dom  43523  tr3dom  43524  fvilbdRP  43686  brtrclfv2  43723  frege110  43969  frege133  43992  k0004lem3  44145  mnuprdlem1  44268  mnuprdlem2  44269  snelpwrVD  44827  nregmodelf1o  45012  fnchoice  45030  elmapsnd  45205  difmapsn  45213  unirnmapsn  45215  ssmapsn  45217  limcresiooub  45647  limcresioolb  45648  cnfdmsn  45887  dvsinax  45918  fourierdlem48  46159  fourierdlem49  46160  sge0sn  46384  sge0p1  46419  ovnovollem1  46661  ovnovollem2  46662  vonvolmbllem  46665  fsetsnf  47056  fsetsnf1  47057  fsetsnfo  47058  cfsetsnfsetfo  47065  setsv  47383  nnsum3primesprm  47795  mapsnop  48336  lindsrng01  48461  snlindsntorlem  48463  snlindsntor  48464  lmod1lem1  48480  lmod1lem2  48481  lmod1lem3  48482  lmod1lem4  48483  lmod1lem5  48484  lmod1  48485  lmod1zr  48486  fv1arycl  48630  1arympt1fv  48632  1arymaptfo  48636  eufsn2  48835  discsubclem  49056  discsubc  49057  iinfconstbas  49059  diag1f1lem  49299  setcsnterm  49483  setc1ocofval  49487  isinito2lem  49491  idfudiag1  49518  diag1f1olem  49526  prstchomval  49552  mndtcbasval  49573  mndtchom  49577  mndtcco  49578  incat  49594  setc1onsubc  49595  aacllem  49794