Theorem snex 4674

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 4619. (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 4023	. . 3 |- { A } = { A , A }
2		preq12 4092	. . . . . 6 |- ( ( x = A /\ x = A ) -> { x , x } = { A , A } )
3	2	anidms 645	. . . . 5 |- ( x = A -> { x , x } = { A , A } )
4	3	eleq1d 2510	. . . 4 |- ( x = A -> ( { x , x } e. _V <-> { A , A } e. _V ) )
5		zfpair2 4673	. . . 4 |- { x , x } e. _V
6	4, 5	vtoclg 3151	. . 3 |- ( A e. _V -> { A , A } e. _V )
7	1, 6	syl5eqel 2533	. 2 |- ( A e. _V -> { A } e. _V )
8		snprc 4074	. . . 4 |- ( -. A e. _V <-> { A } = (/) )
9	8	biimpi 194	. . 3 |- ( -. A e. _V -> { A } = (/) )
10		0ex 4563	. . 3 |- (/) e. _V
11	9, 10	syl6eqel 2537	. 2 |- ( -. A e. _V -> { A } e. _V )
12	7, 11	pm2.61i 164	1 |- { A } e. _V

Syntax hints:   -. wn 3   = wceq 1381   e. wcel 1802   _Vcvv 3093   (/)c0 3767   {csn 4010   {cpr 4012

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pr 4672

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-v 3095  df-dif 3461  df-un 3463  df-nul 3768  df-sn 4011  df-pr 4013

This theorem is referenced by:  prex  4675  elALT  4676  dtruALT2  4677  snelpwi  4678  snelpw  4679  rext  4681  sspwb  4682  intid  4691  moabex  4692  nnullss  4695  exss  4696  opi1  4700  op1stb  4703  opnz  4704  opeqsn  4729  opeqpr  4730  opthwiener  4735  uniop  4736  frirr  4842  frsn  5056  onnev  5070  xpsspwOLD  5103  relop  5139  funopg  5606  tpex  6580  snnex  6587  difsnexi  6589  sucexb  6625  soex  6724  elxp4  6725  elxp5  6726  opabex3d  6759  opabex3  6760  1stval  6783  2ndval  6784  fo1st  6801  fo2nd  6802  mpt2exxg  6855  cnvf1o  6880  fnse  6898  suppsnop  6913  brtpos2  6959  tfrlem12  7056  tfrlem16  7060  mapsn  7458  fvdiagfn  7461  mapsnconst  7462  mapsncnv  7463  mapsnf1o2  7464  ralxpmap  7466  elixpsn  7506  ixpsnf1o  7507  mapsnf1o  7508  ensn1  7577  en1b  7581  mapsnen  7591  xpsnen  7599  endisj  7602  xpsnen2g  7608  domunsncan  7615  enfixsn  7624  domunsn  7665  fodomr  7666  disjenex  7673  domssex2  7675  domssex  7676  map2xp  7685  phplem2  7695  isinf  7731  pssnn  7736  findcard2  7758  ac6sfi  7762  xpfi  7789  fodomfi  7797  pwfilem  7812  fczfsuppd  7845  snopfsupp  7850  fisn  7885  marypha1lem  7891  brwdom2  7997  unxpwdom2  8012  elirrv  8021  epfrs  8160  tc2  8171  tcsni  8172  ranksuc  8281  fseqenlem1  8403  dfac5lem2  8503  dfac5lem3  8504  dfac5lem4  8505  kmlem2  8529  cdafn  8547  cdaval  8548  cdaassen  8560  mapcdaen  8562  cdadom1  8564  cdainf  8570  ackbij1lem5  8602  cfsuc  8635  isfin1-3  8764  hsmexlem4  8807  axcc2lem  8814  dcomex  8825  axdc3lem4  8831  axdc4lem  8833  ttukeylem3  8889  brdom7disj  8907  brdom6disj  8908  fpwwe2lem13  9018  canthwe  9027  canthp1lem1  9028  uniwun  9116  rankcf  9153  nn0ex  10802  hashxplem  12465  hashmap  12467  hashbclem  12475  hashf1lem1  12478  hashge3el3dif  12498  climconst2  13345  incexclem  13622  ramub1lem2  14417  cshwsex  14457  setsvalg  14527  setsid  14545  pwsbas  14756  pwsle  14761  pwssca  14765  pwssnf1o  14767  imasplusg  14786  imasmulr  14787  imasvsca  14789  imasip  14790  xpsc  14826  acsfn  14928  isfunc  15102  homaf  15226  homaval  15227  mgm1  15753  sgrp1  15787  mnd1  15830  mnd1OLD  15831  mnd1id  15832  grp1  16011  symg2bas  16292  idrespermg  16305  pmtrsn  16413  psgnsn  16414  abl1  16741  gsum2d2  16871  gsumcom2  16872  dprdz  16945  dprdsn  16951  dprd2da  16959  ring1  17116  pwssplit3  17575  drngnidl  17745  drnglpir  17769  rng1nnzr  17790  evlssca  18059  mpfind  18073  evls1sca  18228  pf1ind  18259  frlmip  18676  islindf4  18740  mattposvs  18824  mat1dimelbas  18840  mat1dimscm  18844  mat1dimmul  18845  mat1rhmval  18848  m1detdiag  18966  mdetrlin  18971  mdetrsca2  18973  mdetrlin2  18976  mdetunilem5  18985  smadiadetglem2  19041  basdif0  19321  ordtbas  19559  leordtval2  19579  dishaus  19749  discmp  19764  concompid  19798  dis2ndc  19827  dislly  19864  dis1stc  19866  unisngl  19894  1stckgen  19921  ptbasfi  19948  dfac14lem  19984  dfac14  19985  ptrescn  20006  xkoptsub  20021  pt1hmeo  20173  xpstopnlem1  20176  ptcmpfi  20180  isufil2  20275  ufileu  20286  filufint  20287  uffix  20288  uffixsn  20292  flimclslem  20351  ptcmplem1  20418  cnextfval  20428  imasdsf1olem  20742  icccmplem1  21193  icccmplem2  21194  rrxip  21688  elply2  22459  plyss  22462  plyeq0lem  22473  taylfval  22619  axlowdimlem15  24124  axlowdim  24129  umgra1  24191  uslgra1  24237  usgra1  24238  usgra1v  24255  cusgra1v  24326  uvtx01vtx  24357  wlkntrl  24429  0pthonv  24448  constr1trl  24455  1pthon  24458  1pthon2v  24460  1conngra  24540  vdgr1d  24768  vdgr1b  24769  vdgr1a  24771  grposn  25082  zrdivrng  25299  0ofval  25567  resf1o  27418  ordtconlem1  27772  esumpr  27939  esumfzf  27941  prsiga  27997  cntnevol  28065  eulerpartlemgs2  28185  ccatmulgnn0dir  28362  ofs1  28365  ofcs1  28366  subfacp1lem5  28494  erdszelem5  28505  erdszelem8  28508  cvmliftlem4  28599  cvmliftlem5  28600  cvmlift2lem6  28619  cvmlift2lem9  28622  cvmlift2lem12  28625  wfrlem15  29325  fobigcup  29518  elsingles  29536  fnsingle  29537  fvsingle  29538  dfiota3  29541  brapply  29556  brsuccf  29559  funpartlem  29560  altopthsn  29579  altxpsspw  29595  hfsn  29804  onpsstopbas  29863  finixpnum  30006  ptrest  30016  neibastop2lem  30146  topjoin  30151  fdc  30206  heiborlem3  30277  heiborlem8  30282  ismrer1  30302  elrfi  30594  mzpincl  30634  mzpcompact2lem  30652  wopprc  30940  dfac11  30976  kelac2  30979  pwslnmlem1  31006  pwslnm  31008  fnchoice  31351  limcresiooub  31552  limcresioolb  31553  cnfdmsn  31587  dvsinax  31608  fourierdlem48  31822  fourierdlem49  31823  mpt2exxg2  32635  mapsnop  32642  lindsrng01  32779  snlindsntorlem  32781  snlindsntor  32782  lmod1lem1  32798  lmod1lem2  32799  lmod1lem3  32800  lmod1lem4  32801  lmod1lem5  32802  lmod1  32803  lmod1zr  32804  snelpwrVD  33339  bnj918  33531  bnj95  33629  bnj1452  33815  bnj1489  33819  bj-sels  34232  bj-snsetex  34233  bj-elsngl  34238  bj-2uplex  34292  bj-elopg  34305  ldualset  34552  lineset  35164  ispointN  35168  dvaset  36433  dvhset  36510  dibval  36571  dibfna  36583