Theorem snex 1859

Description: A singleton is a set. Theorem 7.13 of [Quine] p. 51, but proved using only Extensionality, Power Set, and Separation.

Assertion

Ref	Expression
snex	|- {A} e. V

Proof of Theorem snex

Step	Hyp	Ref	Expression
1		sneq 1816	. . . 4 |- (x = A -> {x} = {A})
2	1	eleq1d 1155	. . 3 |- (x = A -> ({x} e. V <-> {A} e. V))
3		visset 1350	. . . . 5 |- x e. V
4	3	pwex 1806	. . . 4 |- P~x e. V
5		snsspw 1857	. . . 4 |- {x} (_ P~x
6	4, 5	ssexi 1701	. . 3 |- {x} e. V
7	2, 6	vtoclg 1383	. 2 |- (A e. V -> {A} e. V)
8		snprc 1838	. . 3 |- (-. A e. V <-> {A} = (/))
9		0ex 1745	. . . 4 |- (/) e. V
10		eleq1 1149	. . . 4 |- ({A} = (/) -> ({A} e. V <-> (/) e. V))
11	9, 10	mpbiri 169	. . 3 |- ({A} = (/) -> {A} e. V)
12	8, 11	sylbi 174	. 2 |- (-. A e. V -> {A} e. V)
13	7, 12	pm2.61i 110	1 |- {A} e. V

Syntax hints:  -. wn 1   = wceq 1091   e. wcel 1092  Vcvv 1348  (/)c0 1707  P~cpw 1798  {csn 1808

This theorem is referenced by:  el 1860  snelpw 1861  rext 1862  sspwb 1863  moabex 1868  nnullss 1880  exss 1881  p0ex 1885  prex 1892  opi1 1895  opth 1898  opprc3 1908  opth2 1909  opthwiener 1914  unop 1931  tpex 1952  unipw 1960  op1stb 1992  frirr 2176  sucexb 2301  xpex 2488  elxp4 2640  elxp5 2641  1stval 3089  2ndval 3090  fo1st 3094  fo2nd 3095  map0 3268  mapsn 3269  ensn1 3329  mapsnen 3334  xpsnen 3339  endisj 3341  xpcomen 3343  xpdom2 3345  xpdom3 3347  xpmapenlem2 3392  xpmapenlem4 3394  phplem3 3405  pssnn 3428  eirrv 3449  zfregs 3491  ranksn 3532  rankpr 3536  aceq5lem2 3559  aceq5lem3 3560  kmlem2 3581  fodomb 3615  cardsn 3640  unxpdom2 3651  sucxpdom 3652  cfsuc 3709  cdavalt 3716  uncdadom 3718  cdaassen 3725  xpcdaen 3726  cdadom1 3727  expp1t 4678  exp1t 4679  clim0 4882  climuni 4884  ruclem5 4889  hlim0 5140  hlimcau 5142  hlimuni 5144

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811

metamath.org