Theorem snex 4658

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 4606. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) (Proof modification is discouraged.)

Assertion

Ref	Expression
snex	|- { A } e. _V

Proof of Theorem snex

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfsn2 3993	. . 3 |- { A } = { A , A }
2		preq12 4066	. . . . . 6 |- ( ( x = A /\ x = A ) -> { x , x } = { A , A } )
3	2	anidms 655	. . . . 5 |- ( x = A -> { x , x } = { A , A } )
4	3	eleq1d 2524	. . . 4 |- ( x = A -> ( { x , x } e. _V <-> { A , A } e. _V ) )
5		zfpair2 4657	. . . 4 |- { x , x } e. _V
6	4, 5	vtoclg 3119	. . 3 |- ( A e. _V -> { A , A } e. _V )
7	1, 6	syl5eqel 2544	. 2 |- ( A e. _V -> { A } e. _V )
8		snprc 4048	. . . 4 |- ( -. A e. _V <-> { A } = (/) )
9	8	biimpi 199	. . 3 |- ( -. A e. _V -> { A } = (/) )
10		0ex 4551	. . 3 |- (/) e. _V
11	9, 10	syl6eqel 2548	. 2 |- ( -. A e. _V -> { A } e. _V )
12	7, 11	pm2.61i 169	1 |- { A } e. _V

Syntax hints:   -. wn 3   = wceq 1455   e. wcel 1898   _Vcvv 3057   (/)c0 3743   {csn 3980   {cpr 3982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pr 4656

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-v 3059  df-dif 3419  df-un 3421  df-nul 3744  df-sn 3981  df-pr 3983

This theorem is referenced by:  prex  4659  elALT  4660  dtruALT2  4661  snelpwi  4662  snelpw  4663  rext  4665  sspwb  4666  intid  4675  moabex  4676  nnullss  4679  exss  4680  elopg  4683  opi1  4686  op1stb  4689  opnz  4690  opeqsn  4714  opeqpr  4715  opthwiener  4720  uniop  4721  frirr  4833  frsn  4927  xpsspw  4970  relop  5007  onnev  5566  funopg  5637  fsnex  6211  tpex  6622  snnex  6629  difsnexi  6631  sucexb  6668  soex  6768  elxp4  6769  elxp5  6770  opabex3d  6803  opabex3  6804  1stval  6827  2ndval  6828  fo1st  6845  fo2nd  6846  mpt2exxg  6899  cnvf1o  6927  fnse  6945  suppsnop  6960  brtpos2  7010  wfrlem15  7081  tfrlem12  7138  tfrlem16  7142  mapsn  7544  fvdiagfn  7547  mapsnconst  7548  mapsncnv  7549  mapsnf1o2  7550  ralxpmap  7552  elixpsn  7592  ixpsnf1o  7593  mapsnf1o  7594  ensn1  7664  en1b  7668  mapsnen  7678  xpsnen  7687  endisj  7690  xpsnen2g  7696  domunsncan  7703  enfixsn  7712  domunsn  7753  fodomr  7754  disjenex  7761  domssex2  7763  domssex  7764  map2xp  7773  phplem2  7783  isinf  7816  pssnn  7821  findcard2  7842  ac6sfi  7846  xpfi  7873  fodomfi  7881  pwfilem  7899  fczfsuppd  7932  snopfsupp  7937  fisn  7972  marypha1lem  7978  brwdom2  8119  unxpwdom2  8134  elirrv  8143  epfrs  8246  tc2  8257  tcsni  8258  ranksuc  8367  fseqenlem1  8486  dfac5lem2  8586  dfac5lem3  8587  dfac5lem4  8588  kmlem2  8612  cdafn  8630  cdaval  8631  cdaassen  8643  mapcdaen  8645  cdadom1  8647  cdainf  8653  ackbij1lem5  8685  cfsuc  8718  isfin1-3  8847  hsmexlem4  8890  axcc2lem  8897  dcomex  8908  axdc3lem4  8914  axdc4lem  8916  ttukeylem3  8972  brdom7disj  8990  brdom6disj  8991  fpwwe2lem13  9098  canthwe  9107  canthp1lem1  9108  uniwun  9196  rankcf  9233  nn0ex  10909  hashxplem  12644  hashmap  12646  hashbclem  12654  hashf1lem1  12657  hashge3el3dif  12681  climconst2  13667  incexclem  13949  ramub1lem2  15040  cshwsex  15126  setsvalg  15200  setsid  15219  pwsbas  15440  pwsle  15445  pwssca  15449  pwssnf1o  15451  imasplusg  15473  imasmulr  15474  imasvsca  15476  imasip  15477  xpsc  15518  acsfn  15620  isfunc  15824  homaf  15980  homaval  15981  funcsetcestrclem1  16094  mgm1  16555  sgrp1  16589  mnd1  16632  mnd1OLD  16633  mnd1id  16634  grp1  16813  symg2bas  17094  idrespermg  17107  pmtrsn  17215  psgnsn  17216  abl1  17559  gsum2d2  17661  gsumcom2  17662  dprdz  17718  dprdsn  17724  dprd2da  17730  ring1  17885  pwssplit3  18339  drngnidl  18508  drnglpir  18532  rng1nnzr  18553  evlssca  18800  mpfind  18814  evls1sca  18967  pf1ind  18998  frlmip  19391  islindf4  19451  mattposvs  19535  mat1dimelbas  19551  mat1dimscm  19555  mat1dimmul  19556  mat1rhmval  19559  m1detdiag  19677  mdetrlin  19682  mdetrsca2  19684  mdetrlin2  19687  mdetunilem5  19696  smadiadetglem2  19752  basdif0  20023  ordtbas  20263  leordtval2  20283  dishaus  20453  discmp  20468  concompid  20501  dis2ndc  20530  dislly  20567  dis1stc  20569  unisngl  20597  1stckgen  20624  ptbasfi  20651  dfac14lem  20687  dfac14  20688  ptrescn  20709  xkoptsub  20724  pt1hmeo  20876  xpstopnlem1  20879  ptcmpfi  20883  isufil2  20978  ufileu  20989  filufint  20990  uffix  20991  uffixsn  20995  flimclslem  21054  ptcmplem1  21122  cnextfval  21132  imasdsf1olem  21443  icccmplem1  21895  icccmplem2  21896  rrxip  22404  elply2  23206  plyss  23209  plyeq0lem  23220  taylfval  23370  axlowdimlem15  25042  axlowdim  25047  umgra1  25109  uslgra1  25155  usgra1  25156  usgra1v  25173  cusgra1v  25245  uvtx01vtx  25276  wlkntrl  25348  0pthonv  25367  constr1trl  25374  1pthon  25377  1pthon2v  25379  1conngra  25459  vdgr1d  25687  vdgr1b  25688  vdgr1a  25690  grposn  25999  zrdivrng  26216  0ofval  26484  resf1o  28367  ordtconlem1  28781  esumpr  28938  esumrnmpt2  28940  esumfzf  28941  esum2dlem  28964  esum2d  28965  esumiun  28966  prsiga  29004  rossros  29053  cntnevol  29101  carsgclctunlem1  29199  omsmeas  29205  omsmeasOLD  29206  eulerpartlemgs2  29263  ccatmulgnn0dir  29478  ofs1  29481  ofcs1  29482  bnj918  29627  bnj95  29725  bnj1452  29911  bnj1489  29915  subfacp1lem5  29957  erdszelem5  29968  erdszelem8  29971  cvmliftlem4  30061  cvmliftlem5  30062  cvmlift2lem6  30081  cvmlift2lem9  30084  cvmlift2lem12  30087  fobigcup  30717  elsingles  30735  fnsingle  30736  fvsingle  30737  dfiota3  30740  brapply  30755  brsuccf  30758  funpartlem  30759  altopthsn  30778  altxpsspw  30794  hfsn  30996  neibastop2lem  31066  topjoin  31071  onpsstopbas  31140  bj-sels  31602  bj-snsetex  31603  bj-elsngl  31608  bj-2uplex  31662  f1omptsnlem  31784  mptsnunlem  31786  topdifinffinlem  31796  finixpnum  31976  ptrest  31985  poimirlem3  31989  poimirlem4  31990  poimirlem28  32014  fdc  32120  heiborlem3  32191  heiborlem8  32196  ismrer1  32216  ldualset  32737  lineset  33349  ispointN  33353  dvaset  34618  dvhset  34695  dibval  34756  dibfna  34768  elrfi  35582  mzpincl  35622  mzpcompact2lem  35639  wopprc  35931  dfac11  35966  kelac2  35969  pwslnmlem1  35996  pwslnm  35998  fvilbdRP  36328  brtrclfv2  36365  frege110  36615  frege133  36638  snelpwrVD  37268  fnchoice  37391  mapsnd  37530  mapsnend  37534  mpct  37536  elmapsnd  37539  difmapsn  37550  unirnmapsn  37552  ssmapsn  37554  limcresiooub  37809  limcresioolb  37810  cnfdmsn  37845  dvsinax  37869  fourierdlem48  38119  fourierdlem49  38120  salexct3  38302  salgencntex  38303  salgensscntex  38304  sge0sn  38324  sge0p1  38359  sge0xp  38374  ovnovollem1  38585  ovnovollem2  38586  vonvolmbllem  38589  nnsum3primesprm  39020  propssopi  39137  funsneqopsn  39161  funsneqop  39162  snstrvtxval  39279  snstriedgval  39280  vtxvalsnop  39283  iedgvalsnop  39284  upgr1eop  39347  upgr1eopALT  39349  uspgr1eop  39468  usgr1eop  39471  usgr1vr  39475  uspgrloopvtx  39699  uspgrloopedg  39701  uspgrloopvd2  39703  is01wlk  39930  is0Trl  39935  0pthonv-av  39941  mpt2exxg2  40488  mapsnop  40495  lindsrng01  40630  snlindsntorlem  40632  snlindsntor  40633  lmod1lem1  40649  lmod1lem2  40650  lmod1lem3  40651  lmod1lem4  40652  lmod1lem5  40653  lmod1  40654  lmod1zr  40655  aacllem  40909