Theorem snex 5381

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

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2113  Vcvv 3440  ∅c0 4285  {csn 4580

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 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-un 3906  df-nul 4286  df-sn 4581  df-pr 4583

This theorem is referenced by:  prex  5382  elopg  5414  opi1  5416  op1stb  5419  opnz  5421  opeqsng  5451  opeqpr  5453  snopeqop  5454  opthwiener  5462  uniop  5463  0sn0ep  5528  frirr  5600  opthprc  5688  frsn  5712  relop  5799  snsn0non  6443  onnev  6445  funsneqopb  7097  fsnex  7229  tpex  7691  difsnexi  7706  sucexb  7749  elxp4  7864  elxp5  7865  fvclex  7903  1stval  7935  2ndval  7936  fnse  8075  suppsnop  8120  brtpos2  8174  frrlem13  8240  tfrlem12  8320  tfrlem16  8324  1oex  8407  naddunif  8621  mapsnd  8824  fvdiagfn  8829  mapsnconst  8830  mapsncnv  8831  mapsnf1o2  8832  ralxpmap  8834  elixpsn  8875  ixpsnf1o  8876  mapsnf1o  8877  ensn1  8958  2dom  8967  mapsnend  8973  snmapen  8975  en2sn  8978  xpsnen  8989  endisj  8992  xpsnen2g  8998  domunsncan  9005  enfixsn  9014  disjenex  9063  domssex2  9065  domssex  9066  map2xp  9075  pssnn  9093  snnen2o  9145  isinf  9165  ac6sfi  9184  fodomfiOLD  9230  fczfsuppd  9289  snopfsupp  9294  fisn  9330  tc2  9649  tcsni  9650  ranksuc  9777  djuex  9820  fseqenlem1  9934  djuassen  10089  mapdjuen  10091  djudom1  10093  djuinf  10099  ackbij1lem5  10133  cfsuc  10167  dcomex  10357  axdc3lem4  10363  axdc4lem  10365  ttukeylem3  10421  brdom7disj  10441  brdom6disj  10442  fpwwe2lem12  10553  nn0ex  12407  hashxplem  14356  hashf1lem1  14378  hashge3el3dif  14410  ofs1  14893  climconst2  15471  ramub1lem2  16955  cshwsex  17028  setsvalg  17093  setsid  17134  pwsbas  17407  pwsle  17413  pwssca  17417  pwssnf1o  17419  imasplusg  17438  imasmulr  17439  imasvsca  17441  imasip  17442  acsfn  17582  homaval  17955  funcsetcestrclem1  18077  mgm1  18583  sgrp1  18654  mnd1  18704  mnd1id  18705  efmnd1bas  18818  idresefmnd  18824  smndex1bas  18831  smndex1sgrp  18833  smndex1mnd  18835  smndex1id  18836  grp1  18977  grp1inv  18978  mulgfval  18999  triv1nsgd  19102  1nsgtrivd  19103  symg2bas  19322  idrespermg  19340  pmtrsn  19448  psgnsn  19449  abl1  19795  dprdz  19961  dprdsn  19967  simpgnsgd  20031  2nsgsimpgd  20033  ring1  20245  rng1nnzr  20708  pwssplit3  21013  cnfldex  21312  pzriprnglem13  21448  pzriprnglem14  21449  frlmip  21733  islindf4  21793  evlsvvval  22048  evlssca  22049  psdmul  22109  evls1sca  22267  mattposvs  22399  mat1dimelbas  22415  mat1dimscm  22419  mat1dimmul  22420  mat1rhmval  22423  m1detdiag  22541  mdetrlin  22546  mdetrsca2  22548  mdetrlin2  22551  mdetunilem5  22560  smadiadetglem2  22616  basdif0  22897  ordtbas  23136  leordtval2  23156  conncompid  23375  ptbasfi  23525  dfac14lem  23561  dfac14  23562  ptrescn  23583  xkoptsub  23598  pt1hmeo  23750  xpstopnlem1  23753  ufileu  23863  filufint  23864  uffix  23865  uffixsn  23869  flimclslem  23928  ptcmplem1  23996  imasdsf1olem  24317  icccmplem1  24767  icccmplem2  24768  rrxip  25346  rrxsca  25352  ehl1eudis  25376  elply2  26157  plyss  26160  plyeq0lem  26171  taylfval  26322  sltssnb  27765  lesrec  27795  eqcuts3  27800  0lt1s  27808  sltsleft  27856  sltsright  27857  addsval  27958  addsuniflem  27997  negsid  28037  negsunif  28051  mulsval  28105  sltmuls1  28143  sltmuls2  28144  precsexlem1  28203  precsexlem2  28204  precsexlem11  28213  n0fincut  28351  axlowdimlem15  29029  axlowdim  29034  snstriedgval  29111  vtxvalsnop  29114  iedgvalsnop  29115  upgr1eop  29188  upgr1eopALT  29190  uspgr1eop  29320  usgr1eop  29323  1loopgrvd2  29577  1loopgrvd0  29578  p1evtxdeqlem  29586  p1evtxdeq  29587  p1evtxdp1  29588  uspgrloopvtx  29589  uspgrloopiedg  29591  uspgrloopedg  29592  wlkp1lem4  29748  0pthonv  30204  eupth2lem3  30311  wlkl0  30442  0ofval  30862  suppovss  32760  resf1o  32809  elrgspnlem4  33327  elrspunsn  33510  drngidlhash  33515  zar0ring  34035  ordtconnlem1  34081  esumpr  34223  esumrnmpt2  34225  esumfzf  34226  prsiga  34288  rossros  34337  cntnevol  34385  omsmeas  34480  ccatmulgnn0dir  34699  ofcs1  34701  actfunsnf1o  34761  actfunsnrndisj  34762  reprsuc  34772  breprexplema  34787  bnj918  34922  bnj95  35020  bnj1489  35212  fineqvac  35272  subfacp1lem5  35378  erdszelem5  35389  erdszelem8  35392  cvmliftlem4  35482  cvmliftlem5  35483  cvmlift2lem6  35502  cvmlift2lem9  35505  cvmlift2lem12  35508  satfv1lem  35556  prv1n  35625  brapply  36130  lemsuccf  36133  altopthsn  36155  hfsn  36373  neibastop2lem  36554  topjoin  36559  onpsstopbas  36624  weiunse  36662  bj-2uplex  37223  bj-restsn  37287  finixpnum  37806  ptrest  37820  poimirlem3  37824  poimirlem4  37825  poimirlem28  37849  fdc  37946  heiborlem8  38019  ismrer1  38039  grposnOLD  38083  zrdivrng  38154  ldualset  39385  lineset  39998  dvaset  41265  dvhset  41341  dibval  41402  dibfna  41414  sticksstones9  42408  frlmsnic  42795  evlsevl  42817  elrfi  42936  wopprc  43272  dfac11  43304  kelac2  43307  safesnsupfidom1o  43658  sn1dom  43767  pr2dom  43768  tr3dom  43769  fvilbdRP  43931  brtrclfv2  43968  frege110  44214  frege133  44237  k0004lem3  44390  mnuprdlem1  44513  mnuprdlem2  44514  snelpwrVD  45071  nregmodelf1o  45256  fnchoice  45274  elmapsnd  45448  difmapsn  45456  unirnmapsn  45458  ssmapsn  45460  limcresiooub  45886  limcresioolb  45887  cnfdmsn  46126  dvsinax  46157  fourierdlem48  46398  fourierdlem49  46399  sge0sn  46623  sge0p1  46658  ovnovollem1  46900  ovnovollem2  46901  vonvolmbllem  46904  nthrucw  47130  fsetsnf  47297  fsetsnf1  47298  fsetsnfo  47299  cfsetsnfsetfo  47306  setsv  47624  nnsum3primesprm  48036  mapsnop  48590  lindsrng01  48714  snlindsntorlem  48716  snlindsntor  48717  lmod1lem1  48733  lmod1lem2  48734  lmod1lem3  48735  lmod1lem4  48736  lmod1lem5  48737  lmod1  48738  lmod1zr  48739  fv1arycl  48883  1arympt1fv  48885  1arymaptfo  48889  eufsn2  49088  discsubclem  49308  discsubc  49309  iinfconstbas  49311  diag1f1lem  49551  setcsnterm  49735  setc1ocofval  49739  isinito2lem  49743  idfudiag1  49770  diag1f1olem  49778  prstchomval  49804  mndtcbasval  49825  mndtchom  49829  mndtcco  49830  incat  49846  setc1onsubc  49847  aacllem  50046