Theorem snex 4697

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 4642. (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 4045	. . 3 |- { A } = { A , A }
2		preq12 4113	. . . . . 6 |- ( ( x = A /\ x = A ) -> { x , x } = { A , A } )
3	2	anidms 645	. . . . 5 |- ( x = A -> { x , x } = { A , A } )
4	3	eleq1d 2526	. . . 4 |- ( x = A -> ( { x , x } e. _V <-> { A , A } e. _V ) )
5		zfpair2 4696	. . . 4 |- { x , x } e. _V
6	4, 5	vtoclg 3167	. . 3 |- ( A e. _V -> { A , A } e. _V )
7	1, 6	syl5eqel 2549	. 2 |- ( A e. _V -> { A } e. _V )
8		snprc 4095	. . . 4 |- ( -. A e. _V <-> { A } = (/) )
9	8	biimpi 194	. . 3 |- ( -. A e. _V -> { A } = (/) )
10		0ex 4587	. . 3 |- (/) e. _V
11	9, 10	syl6eqel 2553	. 2 |- ( -. A e. _V -> { A } e. _V )
12	7, 11	pm2.61i 164	1 |- { A } e. _V

Syntax hints:   -. wn 3   = wceq 1395   e. wcel 1819   _Vcvv 3109   (/)c0 3793   {csn 4032   {cpr 4034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pr 4695

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3474  df-un 3476  df-nul 3794  df-sn 4033  df-pr 4035

This theorem is referenced by:  prex  4698  elALT  4699  dtruALT2  4700  snelpwi  4701  snelpw  4702  rext  4704  sspwb  4705  intid  4714  moabex  4715  nnullss  4718  exss  4719  opi1  4723  op1stb  4726  opnz  4727  opeqsn  4752  opeqpr  4753  opthwiener  4758  uniop  4759  frirr  4865  frsn  5079  onnev  5093  xpsspwOLD  5126  relop  5163  funopg  5626  tpex  6598  snnex  6605  difsnexi  6607  sucexb  6643  soex  6742  elxp4  6743  elxp5  6744  opabex3d  6777  opabex3  6778  1stval  6801  2ndval  6802  fo1st  6819  fo2nd  6820  mpt2exxg  6873  cnvf1o  6898  fnse  6916  suppsnop  6931  brtpos2  6979  tfrlem12  7076  tfrlem16  7080  mapsn  7479  fvdiagfn  7482  mapsnconst  7483  mapsncnv  7484  mapsnf1o2  7485  ralxpmap  7487  elixpsn  7527  ixpsnf1o  7528  mapsnf1o  7529  ensn1  7598  en1b  7602  mapsnen  7612  xpsnen  7620  endisj  7623  xpsnen2g  7629  domunsncan  7636  enfixsn  7645  domunsn  7686  fodomr  7687  disjenex  7694  domssex2  7696  domssex  7697  map2xp  7706  phplem2  7716  isinf  7752  pssnn  7757  findcard2  7778  ac6sfi  7782  xpfi  7809  fodomfi  7817  pwfilem  7832  fczfsuppd  7865  snopfsupp  7870  fisn  7905  marypha1lem  7911  brwdom2  8017  unxpwdom2  8032  elirrv  8041  epfrs  8179  tc2  8190  tcsni  8191  ranksuc  8300  fseqenlem1  8422  dfac5lem2  8522  dfac5lem3  8523  dfac5lem4  8524  kmlem2  8548  cdafn  8566  cdaval  8567  cdaassen  8579  mapcdaen  8581  cdadom1  8583  cdainf  8589  ackbij1lem5  8621  cfsuc  8654  isfin1-3  8783  hsmexlem4  8826  axcc2lem  8833  dcomex  8844  axdc3lem4  8850  axdc4lem  8852  ttukeylem3  8908  brdom7disj  8926  brdom6disj  8927  fpwwe2lem13  9037  canthwe  9046  canthp1lem1  9047  uniwun  9135  rankcf  9172  nn0ex  10822  hashxplem  12495  hashmap  12497  hashbclem  12505  hashf1lem1  12508  hashge3el3dif  12528  climconst2  13383  incexclem  13660  ramub1lem2  14557  cshwsex  14597  setsvalg  14668  setsid  14687  pwsbas  14904  pwsle  14909  pwssca  14913  pwssnf1o  14915  imasplusg  14934  imasmulr  14935  imasvsca  14937  imasip  14938  xpsc  14974  acsfn  15076  isfunc  15280  homaf  15436  homaval  15437  funcsetcestrclem1  15550  mgm1  16011  sgrp1  16045  mnd1  16088  mnd1OLD  16089  mnd1id  16090  grp1  16269  symg2bas  16550  idrespermg  16563  pmtrsn  16671  psgnsn  16672  abl1  16999  gsum2d2  17129  gsumcom2  17130  dprdz  17204  dprdsn  17210  dprd2da  17218  ring1  17375  pwssplit3  17834  drngnidl  18004  drnglpir  18028  rng1nnzr  18049  evlssca  18318  mpfind  18332  evls1sca  18487  pf1ind  18518  frlmip  18936  islindf4  19000  mattposvs  19084  mat1dimelbas  19100  mat1dimscm  19104  mat1dimmul  19105  mat1rhmval  19108  m1detdiag  19226  mdetrlin  19231  mdetrsca2  19233  mdetrlin2  19236  mdetunilem5  19245  smadiadetglem2  19301  basdif0  19581  ordtbas  19820  leordtval2  19840  dishaus  20010  discmp  20025  concompid  20058  dis2ndc  20087  dislly  20124  dis1stc  20126  unisngl  20154  1stckgen  20181  ptbasfi  20208  dfac14lem  20244  dfac14  20245  ptrescn  20266  xkoptsub  20281  pt1hmeo  20433  xpstopnlem1  20436  ptcmpfi  20440  isufil2  20535  ufileu  20546  filufint  20547  uffix  20548  uffixsn  20552  flimclslem  20611  ptcmplem1  20678  cnextfval  20688  imasdsf1olem  21002  icccmplem1  21453  icccmplem2  21454  rrxip  21948  elply2  22719  plyss  22722  plyeq0lem  22733  taylfval  22880  axlowdimlem15  24386  axlowdim  24391  umgra1  24453  uslgra1  24499  usgra1  24500  usgra1v  24517  cusgra1v  24588  uvtx01vtx  24619  wlkntrl  24691  0pthonv  24710  constr1trl  24717  1pthon  24720  1pthon2v  24722  1conngra  24802  vdgr1d  25030  vdgr1b  25031  vdgr1a  25033  grposn  25344  zrdivrng  25561  0ofval  25829  resf1o  27710  ordtconlem1  28067  esumpr  28238  esumrnmpt2  28240  esumfzf  28241  esum2dlem  28264  esum2d  28265  esumiun  28266  prsiga  28304  cntnevol  28372  carsgclctunlem1  28460  eulerpartlemgs2  28516  ccatmulgnn0dir  28693  ofs1  28696  ofcs1  28697  subfacp1lem5  28825  erdszelem5  28836  erdszelem8  28839  cvmliftlem4  28930  cvmliftlem5  28931  cvmlift2lem6  28950  cvmlift2lem9  28953  cvmlift2lem12  28956  wfrlem15  29574  fobigcup  29755  elsingles  29773  fnsingle  29774  fvsingle  29775  dfiota3  29778  brapply  29793  brsuccf  29796  funpartlem  29797  altopthsn  29816  altxpsspw  29832  hfsn  30041  onpsstopbas  30100  finixpnum  30243  ptrest  30253  neibastop2lem  30383  topjoin  30388  fdc  30443  heiborlem3  30514  heiborlem8  30519  ismrer1  30539  elrfi  30831  mzpincl  30871  mzpcompact2lem  30889  wopprc  31176  dfac11  31212  kelac2  31215  pwslnmlem1  31242  pwslnm  31244  fnchoice  31607  limcresiooub  31851  limcresioolb  31852  cnfdmsn  31887  dvsinax  31911  fourierdlem48  32140  fourierdlem49  32141  mpt2exxg2  33071  mapsnop  33078  lindsrng01  33213  snlindsntorlem  33215  snlindsntor  33216  lmod1lem1  33232  lmod1lem2  33233  lmod1lem3  33234  lmod1lem4  33235  lmod1lem5  33236  lmod1  33237  lmod1zr  33238  aacllem  33360  snelpwrVD  33774  bnj918  33967  bnj95  34065  bnj1452  34251  bnj1489  34255  bj-sels  34663  bj-snsetex  34664  bj-elsngl  34669  bj-2uplex  34723  bj-elopg  34745  ldualset  34993  lineset  35605  ispointN  35609  dvaset  36874  dvhset  36951  dibval  37012  dibfna  37024