Theorem snex 4681

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 4626. (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 4033	. . 3 |- { A } = { A , A }
2		preq12 4101	. . . . . 6 |- ( ( x = A /\ x = A ) -> { x , x } = { A , A } )
3	2	anidms 645	. . . . 5 |- ( x = A -> { x , x } = { A , A } )
4	3	eleq1d 2529	. . . 4 |- ( x = A -> ( { x , x } e. _V <-> { A , A } e. _V ) )
5		zfpair2 4680	. . . 4 |- { x , x } e. _V
6	4, 5	vtoclg 3164	. . 3 |- ( A e. _V -> { A , A } e. _V )
7	1, 6	syl5eqel 2552	. 2 |- ( A e. _V -> { A } e. _V )
8		snprc 4084	. . . 4 |- ( -. A e. _V <-> { A } = (/) )
9	8	biimpi 194	. . 3 |- ( -. A e. _V -> { A } = (/) )
10		0ex 4570	. . 3 |- (/) e. _V
11	9, 10	syl6eqel 2556	. 2 |- ( -. A e. _V -> { A } e. _V )
12	7, 11	pm2.61i 164	1 |- { A } e. _V

Syntax hints:   -. wn 3   = wceq 1374   e. wcel 1762   _Vcvv 3106   (/)c0 3778   {csn 4020   {cpr 4022

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-v 3108  df-dif 3472  df-un 3474  df-nul 3779  df-sn 4021  df-pr 4023

This theorem is referenced by:  prex  4682  elALT  4683  dtruALT2  4684  snelpwi  4685  snelpw  4686  rext  4688  sspwb  4689  intid  4698  moabex  4699  nnullss  4702  exss  4703  opi1  4707  op1stb  4710  opnz  4711  opeqsn  4736  opeqpr  4737  opthwiener  4742  uniop  4743  frirr  4849  frsn  5062  onnev  5075  xpsspwOLD  5108  relop  5144  funopg  5611  tpex  6574  snnex  6577  difsnexi  6579  sucexb  6615  soex  6717  elxp4  6718  elxp5  6719  opabex3d  6752  opabex3  6753  1stval  6776  2ndval  6777  fo1st  6794  fo2nd  6795  mpt2exxg  6847  cnvf1o  6872  fnse  6890  suppsnop  6905  brtpos2  6951  tfrlem12  7048  tfrlem16  7052  mapsn  7450  fvdiagfn  7453  mapsnconst  7454  mapsncnv  7455  mapsnf1o2  7456  ralxpmap  7458  elixpsn  7498  ixpsnf1o  7499  mapsnf1o  7500  ensn1  7569  en1b  7573  mapsnen  7583  xpsnen  7591  endisj  7594  xpsnen2g  7600  domunsncan  7607  enfixsn  7616  domunsn  7657  fodomr  7658  disjenex  7665  domssex2  7667  domssex  7668  map2xp  7677  phplem2  7687  isinf  7723  pssnn  7728  findcard2  7749  ac6sfi  7753  xpfi  7780  fodomfi  7788  pwfilem  7803  fczfsuppd  7836  snopfsupp  7841  fisn  7876  marypha1lem  7882  brwdom2  7988  unxpwdom2  8003  elirrv  8012  epfrs  8151  tc2  8162  tcsni  8163  ranksuc  8272  fseqenlem1  8394  dfac5lem2  8494  dfac5lem3  8495  dfac5lem4  8496  kmlem2  8520  cdafn  8538  cdaval  8539  cdaassen  8551  mapcdaen  8553  cdadom1  8555  cdainf  8561  ackbij1lem5  8593  cfsuc  8626  isfin1-3  8755  hsmexlem4  8798  axcc2lem  8805  dcomex  8816  axdc3lem4  8822  axdc4lem  8824  ttukeylem3  8880  brdom7disj  8898  brdom6disj  8899  fpwwe2lem13  9009  canthwe  9018  canthp1lem1  9019  uniwun  9107  rankcf  9144  nn0ex  10790  hashxplem  12444  hashmap  12446  hashbclem  12454  hashf1lem1  12457  hashge3el3dif  12477  climconst2  13320  incexclem  13600  ramub1lem2  14393  cshwsex  14432  setsvalg  14502  setsid  14520  pwsbas  14731  pwsle  14736  pwssca  14740  pwssnf1o  14742  imasplusg  14761  imasmulr  14762  imasvsca  14764  imasip  14765  xpsc  14801  acsfn  14903  isfunc  15080  homaf  15204  homaval  15205  symg2bas  16211  idrespermg  16224  pmtrsn  16333  psgnsn  16334  gsum2d2  16786  gsumcom2  16787  dprdz  16860  dprdsn  16866  dprd2da  16874  pwssplit3  17483  drngnidl  17652  drnglpir  17676  evlssca  17955  mpfind  17969  evls1sca  18124  pf1ind  18155  frlmip  18569  islindf4  18633  mattposvs  18717  mat1dimelbas  18733  mat1dimscm  18737  mat1dimmul  18738  mat1rhmval  18741  m1detdiag  18859  mdetrlin  18864  mdetrsca2  18866  mdetrlin2  18869  mdetunilem5  18878  smadiadetglem2  18934  basdif0  19214  ordtbas  19452  leordtval2  19472  dishaus  19642  discmp  19657  concompid  19691  dis2ndc  19720  dislly  19757  dis1stc  19759  1stckgen  19783  ptbasfi  19810  dfac14lem  19846  dfac14  19847  ptrescn  19868  xkoptsub  19883  pt1hmeo  20035  xpstopnlem1  20038  ptcmpfi  20042  isufil2  20137  ufileu  20148  filufint  20149  uffix  20150  uffixsn  20154  flimclslem  20213  ptcmplem1  20280  cnextfval  20290  imasdsf1olem  20604  icccmplem1  21055  icccmplem2  21056  rrxip  21550  elply2  22321  plyss  22324  plyeq0lem  22335  taylfval  22481  axlowdimlem15  23928  axlowdim  23933  umgra1  23989  uslgra1  24034  usgra1  24035  usgra1v  24052  cusgra1v  24123  uvtx01vtx  24154  wlkntrl  24226  0pthonv  24245  constr1trl  24252  1pthon  24255  1pthon2v  24257  1conngra  24337  vdgr1d  24565  vdgr1b  24566  vdgr1a  24568  grposn  24743  zrdivrng  24960  0ofval  25228  resf1o  27075  ordtconlem1  27392  esumpr  27563  esumfzf  27565  prsiga  27621  cntnevol  27689  eulerpartlemgs2  27809  ccatmulgnn0dir  27986  ofs1  27989  ofcs1  27990  subfacp1lem5  28118  erdszelem5  28129  erdszelem8  28132  cvmliftlem4  28223  cvmliftlem5  28224  cvmlift2lem6  28243  cvmlift2lem9  28246  cvmlift2lem12  28249  wfrlem15  28784  fobigcup  28977  elsingles  28995  fnsingle  28996  fvsingle  28997  dfiota3  29000  brapply  29015  brsuccf  29018  funpartlem  29019  altopthsn  29038  altxpsspw  29054  hfsn  29263  onpsstopbas  29322  finixpnum  29465  ptrest  29476  neibastop2lem  29632  topjoin  29637  fdc  29692  heiborlem3  29763  heiborlem8  29768  ismrer1  29788  elrfi  30081  mzpincl  30121  mzpcompact2lem  30139  wopprc  30429  dfac11  30465  kelac2  30468  pwslnmlem1  30495  pwslnm  30497  fnchoice  30801  limcresiooub  31003  limcresioolb  31004  cnfdmsn  31039  dvsinax  31060  fourierdlem48  31274  fourierdlem49  31275  mpt2exxg2  31866  mapsnop  31873  lindsrng01  32017  snlindsntorlem  32019  snlindsntor  32020  mnd1  32036  grp1  32037  abl1  32038  rng1  32040  rng1nnzr  32041  lmod1lem1  32044  lmod1lem2  32045  lmod1lem3  32046  lmod1lem4  32047  lmod1lem5  32048  lmod1  32049  lmod1zr  32050  snelpwrVD  32586  bnj918  32778  bnj95  32876  bnj1452  33062  bnj1489  33066  bj-sels  33476  bj-snsetex  33477  bj-elsngl  33482  bj-2uplex  33536  bj-elopg  33549  ldualset  33797  lineset  34409  ispointN  34413  dvaset  35676  dvhset  35753  dibval  35814  dibfna  35826