Theorem snex 5436

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

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2108  Vcvv 3480  ∅c0 4333  {csn 4626

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-un 3956  df-nul 4334  df-sn 4627  df-pr 4629

This theorem is referenced by:  prex  5437  snelpwiOLD  5449  intidOLD  5463  elopg  5471  opi1  5473  op1stb  5476  opnz  5478  opeqsng  5508  opeqpr  5510  snopeqop  5511  opthwiener  5519  uniop  5520  0sn0ep  5588  frirr  5661  opthprc  5749  frsn  5773  relop  5861  snsn0non  6509  onnev  6511  funsneqopb  7172  fsnex  7303  tpex  7766  difsnexi  7781  sucexb  7824  elxp4  7944  elxp5  7945  fvclex  7983  1stval  8016  2ndval  8017  fnse  8158  suppsnop  8203  brtpos2  8257  frrlem13  8323  wfrlem15OLD  8363  tfrlem12  8429  tfrlem16  8433  1oex  8516  naddunif  8731  mapsnd  8926  fvdiagfn  8931  mapsnconst  8932  mapsncnv  8933  mapsnf1o2  8934  ralxpmap  8936  elixpsn  8977  ixpsnf1o  8978  mapsnf1o  8979  ensn1  9061  2dom  9070  mapsnend  9076  snmapen  9078  en2sn  9081  xpsnen  9095  endisj  9098  xpsnen2g  9105  domunsncan  9112  enfixsn  9121  disjenex  9175  domssex2  9177  domssex  9178  map2xp  9187  pssnn  9208  phplem2OLD  9255  snnen2o  9273  isinf  9296  isinfOLD  9297  ac6sfi  9320  xpfiOLD  9359  fodomfiOLD  9370  fczfsuppd  9426  snopfsupp  9431  fisn  9467  tc2  9782  tcsni  9783  ranksuc  9905  djuex  9948  fseqenlem1  10064  djuassen  10219  mapdjuen  10221  djudom1  10223  djuinf  10229  ackbij1lem5  10263  cfsuc  10297  dcomex  10487  axdc3lem4  10493  axdc4lem  10495  ttukeylem3  10551  brdom7disj  10571  brdom6disj  10572  fpwwe2lem12  10682  nn0ex  12532  hashxplem  14472  hashf1lem1  14494  hashge3el3dif  14526  ofs1  15009  climconst2  15584  ramub1lem2  17065  cshwsex  17138  setsvalg  17203  setsid  17244  pwsbas  17532  pwsle  17537  pwssca  17541  pwssnf1o  17543  imasplusg  17562  imasmulr  17563  imasvsca  17565  imasip  17566  acsfn  17702  homaval  18076  funcsetcestrclem1  18199  mgm1  18671  sgrp1  18742  mnd1  18792  mnd1id  18793  efmnd1bas  18906  idresefmnd  18912  smndex1bas  18919  smndex1sgrp  18921  smndex1mnd  18923  smndex1id  18924  grp1  19065  grp1inv  19066  mulgfval  19087  triv1nsgd  19191  1nsgtrivd  19192  symg2bas  19410  symgvalstructOLD  19415  idrespermg  19429  pmtrsn  19537  psgnsn  19538  abl1  19884  dprdz  20050  dprdsn  20056  simpgnsgd  20120  2nsgsimpgd  20122  ring1  20307  rng1nnzr  20776  pwssplit3  21060  cnfldex  21367  pzriprnglem13  21504  pzriprnglem14  21505  frlmip  21798  islindf4  21858  evlssca  22113  psdmul  22170  evls1sca  22327  mattposvs  22461  mat1dimelbas  22477  mat1dimscm  22481  mat1dimmul  22482  mat1rhmval  22485  m1detdiag  22603  mdetrlin  22608  mdetrsca2  22610  mdetrlin2  22613  mdetunilem5  22622  smadiadetglem2  22678  basdif0  22960  ordtbas  23200  leordtval2  23220  conncompid  23439  ptbasfi  23589  dfac14lem  23625  dfac14  23626  ptrescn  23647  xkoptsub  23662  pt1hmeo  23814  xpstopnlem1  23817  ufileu  23927  filufint  23928  uffix  23929  uffixsn  23933  flimclslem  23992  ptcmplem1  24060  imasdsf1olem  24383  icccmplem1  24844  icccmplem2  24845  rrxip  25424  rrxsca  25430  ehl1eudis  25454  elply2  26235  plyss  26238  plyeq0lem  26249  taylfval  26400  ssltsn  27837  slerec  27864  0slt1s  27874  ssltleft  27909  ssltright  27910  addsval  27995  addsuniflem  28034  negsid  28073  negsunif  28087  mulsval  28135  ssltmul1  28173  ssltmul2  28174  precsexlem1  28231  precsexlem2  28232  precsexlem11  28241  nohalf  28407  0reno  28429  axlowdimlem15  28971  axlowdim  28976  snstriedgval  29055  vtxvalsnop  29058  iedgvalsnop  29059  upgr1eop  29132  upgr1eopALT  29134  uspgr1eop  29264  usgr1eop  29267  1loopgrvd2  29521  1loopgrvd0  29522  p1evtxdeqlem  29530  p1evtxdeq  29531  p1evtxdp1  29532  uspgrloopvtx  29533  uspgrloopiedg  29535  uspgrloopedg  29536  wlkp1lem4  29694  0pthonv  30148  eupth2lem3  30255  wlkl0  30386  0ofval  30806  suppovss  32690  resf1o  32741  elrgspnlem4  33249  elrspunsn  33457  drngidlhash  33462  zar0ring  33877  ordtconnlem1  33923  esumpr  34067  esumrnmpt2  34069  esumfzf  34070  prsiga  34132  rossros  34181  cntnevol  34229  omsmeas  34325  ccatmulgnn0dir  34557  ofcs1  34559  actfunsnf1o  34619  actfunsnrndisj  34620  reprsuc  34630  breprexplema  34645  bnj918  34780  bnj95  34878  bnj1489  35070  fineqvac  35111  subfacp1lem5  35189  erdszelem5  35200  erdszelem8  35203  cvmliftlem4  35293  cvmliftlem5  35294  cvmlift2lem6  35313  cvmlift2lem9  35316  cvmlift2lem12  35319  satfv1lem  35367  prv1n  35436  brapply  35939  brsuccf  35942  altopthsn  35962  hfsn  36180  neibastop2lem  36361  topjoin  36366  onpsstopbas  36431  weiunse  36469  bj-2uplex  37023  bj-restsn  37083  finixpnum  37612  ptrest  37626  poimirlem3  37630  poimirlem4  37631  poimirlem28  37655  fdc  37752  heiborlem8  37825  ismrer1  37845  grposnOLD  37889  zrdivrng  37960  ecexALTV  38332  eccnvepex  38336  ldualset  39126  lineset  39740  dvaset  41007  dvhset  41083  dibval  41144  dibfna  41156  sticksstones9  42155  frlmsnic  42550  evlsvvval  42573  evlsevl  42581  elrfi  42705  wopprc  43042  dfac11  43074  kelac2  43077  safesnsupfidom1o  43430  sn1dom  43539  pr2dom  43540  tr3dom  43541  fvilbdRP  43703  brtrclfv2  43740  frege110  43986  frege133  44009  k0004lem3  44162  mnuprdlem1  44291  mnuprdlem2  44292  snelpwrVD  44851  fnchoice  45034  elmapsnd  45209  difmapsn  45217  unirnmapsn  45219  ssmapsn  45221  limcresiooub  45657  limcresioolb  45658  cnfdmsn  45897  dvsinax  45928  fourierdlem48  46169  fourierdlem49  46170  sge0sn  46394  sge0p1  46429  ovnovollem1  46671  ovnovollem2  46672  vonvolmbllem  46675  fsetsnf  47063  fsetsnf1  47064  fsetsnfo  47065  cfsetsnfsetfo  47072  setsv  47365  nnsum3primesprm  47777  mapsnop  48260  lindsrng01  48385  snlindsntorlem  48387  snlindsntor  48388  lmod1lem1  48404  lmod1lem2  48405  lmod1lem3  48406  lmod1lem4  48407  lmod1lem5  48408  lmod1  48409  lmod1zr  48410  fv1arycl  48558  1arympt1fv  48560  1arymaptfo  48564  eufsn2  48752  setcsnterm  49133  prstchomval  49163  mndtcbasval  49177  mndtchom  49181  mndtcco  49182  aacllem  49320