Theorem snex 5432

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

Syntax hints:  ¬ wn 3   = wceq 1542   ∈ wcel 2107  Vcvv 3475  ∅c0 4323  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-un 3954  df-nul 4324  df-sn 4630  df-pr 4632

This theorem is referenced by:  prex  5433  snelpwiOLD  5445  intidOLD  5459  elopg  5467  opi1  5469  op1stb  5472  opnz  5474  opeqsng  5504  opeqpr  5506  snopeqop  5507  opthwiener  5515  uniop  5516  0sn0ep  5585  frirr  5654  opthprc  5741  frsn  5764  relop  5851  snsn0non  6490  onnev  6492  onnevOLD  6493  funsneqopb  7150  fsnex  7281  tpex  7734  difsnexi  7748  sucexb  7792  elxp4  7913  elxp5  7914  fvclex  7945  1stval  7977  2ndval  7978  fnse  8119  suppsnop  8163  brtpos2  8217  frrlem13  8283  wfrlem15OLD  8323  tfrlem12  8389  tfrlem16  8393  1oex  8476  naddunif  8692  mapsnd  8880  fvdiagfn  8885  mapsnconst  8886  mapsncnv  8887  mapsnf1o2  8888  ralxpmap  8890  elixpsn  8931  ixpsnf1o  8932  mapsnf1o  8933  ensn1  9017  ensn1OLD  9018  en1bOLD  9024  2dom  9030  mapsnend  9036  snmapen  9038  en2sn  9041  en2snOLD  9042  xpsnen  9055  endisj  9058  xpsnen2g  9065  domunsncan  9072  enfixsn  9081  disjenex  9135  domssex2  9137  domssex  9138  map2xp  9147  pssnn  9168  phplem2OLD  9218  snnen2o  9237  isinf  9260  isinfOLD  9261  pssnnOLD  9265  findcard2OLD  9284  ac6sfi  9287  xpfiOLD  9318  fodomfi  9325  pwfilemOLD  9346  fczfsuppd  9381  snopfsupp  9386  fisn  9422  tc2  9737  tcsni  9738  ranksuc  9860  djuex  9903  fseqenlem1  10019  djuassen  10173  mapdjuen  10175  djudom1  10177  djuinf  10183  ackbij1lem5  10219  cfsuc  10252  dcomex  10442  axdc3lem4  10448  axdc4lem  10450  ttukeylem3  10506  brdom7disj  10526  brdom6disj  10527  fpwwe2lem12  10637  nn0ex  12478  hashxplem  14393  hashf1lem1  14415  hashf1lem1OLD  14416  hashge3el3dif  14447  ofs1  14917  climconst2  15492  ramub1lem2  16960  cshwsex  17034  setsvalg  17099  setsid  17141  pwsbas  17433  pwsle  17438  pwssca  17442  pwssnf1o  17444  imasplusg  17463  imasmulr  17464  imasvsca  17466  imasip  17467  acsfn  17603  homaval  17981  funcsetcestrclem1  18106  mgm1  18577  sgrp1  18620  mnd1  18667  mnd1id  18668  efmnd1bas  18774  idresefmnd  18780  smndex1bas  18787  smndex1sgrp  18789  smndex1mnd  18791  smndex1id  18792  grp1  18930  grp1inv  18931  mulgfval  18952  triv1nsgd  19053  1nsgtrivd  19054  symg2bas  19260  symgvalstructOLD  19265  idrespermg  19279  pmtrsn  19387  psgnsn  19388  abl1  19734  dprdz  19900  dprdsn  19906  simpgnsgd  19970  2nsgsimpgd  19972  ring1  20122  rng1nnzr  20396  pwssplit3  20672  frlmip  21333  islindf4  21393  evlssca  21652  evls1sca  21842  mattposvs  21957  mat1dimelbas  21973  mat1dimscm  21977  mat1dimmul  21978  mat1rhmval  21981  m1detdiag  22099  mdetrlin  22104  mdetrsca2  22106  mdetrlin2  22109  mdetunilem5  22118  smadiadetglem2  22174  basdif0  22456  ordtbas  22696  leordtval2  22716  conncompid  22935  ptbasfi  23085  dfac14lem  23121  dfac14  23122  ptrescn  23143  xkoptsub  23158  pt1hmeo  23310  xpstopnlem1  23313  ufileu  23423  filufint  23424  uffix  23425  uffixsn  23429  flimclslem  23488  ptcmplem1  23556  imasdsf1olem  23879  icccmplem1  24338  icccmplem2  24339  rrxip  24907  rrxsca  24913  ehl1eudis  24937  elply2  25710  plyss  25713  plyeq0lem  25724  taylfval  25871  slerec  27320  0slt1s  27330  ssltleft  27365  ssltright  27366  addsval  27446  addsuniflem  27484  negsid  27515  negsunif  27529  mulsval  27565  ssltmul1  27602  ssltmul2  27603  precsexlem1  27653  precsexlem2  27654  precsexlem11  27663  axlowdimlem15  28214  axlowdim  28219  snstriedgval  28298  vtxvalsnop  28301  iedgvalsnop  28302  upgr1eop  28375  upgr1eopALT  28377  uspgr1eop  28504  usgr1eop  28507  1loopgrvd2  28760  1loopgrvd0  28761  p1evtxdeqlem  28769  p1evtxdeq  28770  p1evtxdp1  28771  uspgrloopvtx  28772  uspgrloopiedg  28774  uspgrloopedg  28775  wlkp1lem4  28933  0pthonv  29382  eupth2lem3  29489  wlkl0  29620  0ofval  30040  suppovss  31906  resf1o  31955  elrspunsn  32547  drngidlhash  32552  zar0ring  32858  ordtconnlem1  32904  esumpr  33064  esumrnmpt2  33066  esumfzf  33067  prsiga  33129  rossros  33178  cntnevol  33226  omsmeas  33322  ccatmulgnn0dir  33553  ofcs1  33555  actfunsnf1o  33616  actfunsnrndisj  33617  reprsuc  33627  breprexplema  33642  bnj918  33777  bnj95  33875  bnj1489  34067  fineqvac  34097  subfacp1lem5  34175  erdszelem5  34186  erdszelem8  34189  cvmliftlem4  34279  cvmliftlem5  34280  cvmlift2lem6  34299  cvmlift2lem9  34302  cvmlift2lem12  34305  satfv1lem  34353  prv1n  34422  brapply  34910  brsuccf  34913  altopthsn  34933  hfsn  35151  gg-cnfldex  35180  neibastop2lem  35245  topjoin  35250  onpsstopbas  35315  bj-2uplex  35903  bj-restsn  35963  finixpnum  36473  ptrest  36487  poimirlem3  36491  poimirlem4  36492  poimirlem28  36516  fdc  36613  heiborlem8  36686  ismrer1  36706  grposnOLD  36750  zrdivrng  36821  ecexALTV  37200  eccnvepex  37204  ldualset  37995  lineset  38609  dvaset  39876  dvhset  39952  dibval  40013  dibfna  40025  sticksstones9  40970  frlmsnic  41110  evlsvvval  41135  evlsevl  41143  elrfi  41432  wopprc  41769  dfac11  41804  kelac2  41807  safesnsupfidom1o  42168  sn1dom  42277  pr2dom  42278  tr3dom  42279  fvilbdRP  42441  brtrclfv2  42478  frege110  42724  frege133  42747  k0004lem3  42900  mnuprdlem1  43031  mnuprdlem2  43032  snelpwrVD  43592  fnchoice  43713  elmapsnd  43903  difmapsn  43911  unirnmapsn  43913  ssmapsn  43915  limcresiooub  44358  limcresioolb  44359  cnfdmsn  44598  dvsinax  44629  fourierdlem48  44870  fourierdlem49  44871  sge0sn  45095  sge0p1  45130  ovnovollem1  45372  ovnovollem2  45373  vonvolmbllem  45376  fsetsnf  45761  fsetsnf1  45762  fsetsnfo  45763  cfsetsnfsetfo  45770  setsv  46046  nnsum3primesprm  46458  pzriprnglem13  46817  pzriprnglem14  46818  mapsnop  47020  lindsrng01  47149  snlindsntorlem  47151  snlindsntor  47152  lmod1lem1  47168  lmod1lem2  47169  lmod1lem3  47170  lmod1lem4  47171  lmod1lem5  47172  lmod1  47173  lmod1zr  47174  fv1arycl  47323  1arympt1fv  47325  1arymaptfo  47329  eufsn2  47509  prstchomval  47694  mndtcbasval  47706  mndtchom  47710  mndtcco  47711  aacllem  47848