Theorem snex 2766

Description: A singleton is a set. Theorem 7.13 of [Quine] p. 51, but proved using only Extensionality, Power Set, and Separation. Unlike the proof of zfpair 2793, Replacement is not needed.

Assertion

Ref	Expression
snex	⊢ {A} ∈ V

Proof of Theorem snex

Step	Hyp	Ref	Expression
1		sneq 2429	. . . 4 ⊢ (x = A → {x} = {A})
2	1	eleq1d 1547	. . 3 ⊢ (x = A → ({x} ∈ V ↔ {A} ∈ V))
3		visset 1820	. . . . 5 ⊢ x ∈ V
4	3	pwex 2761	. . . 4 ⊢ ℘x ∈ V
5		snsspw 2493	. . . 4 ⊢ {x} ⊆ ℘x
6	4, 5	ssexi 2735	. . 3 ⊢ {x} ∈ V
7	2, 6	vtoclg 1854	. 2 ⊢ (A ∈ V → {A} ∈ V)
8		snprc 2455	. . 3 ⊢ (¬ A ∈ V ↔ {A} = ∅)
9		axnul 2724	. . . . . . 7 ⊢ ∃x∀y ¬ y ∈ x
10	9	zfnuleu 2722	. . . . . 6 ⊢ ∃!x∀y ¬ y ∈ x
11		eq0 2306	. . . . . . 7 ⊢ (x = ∅ ↔ ∀y ¬ y ∈ x)
12	11	eubii 1391	. . . . . 6 ⊢ (∃!x x = ∅ ↔ ∃!x∀y ¬ y ∈ x)
13	10, 12	mpbir 190	. . . . 5 ⊢ ∃!x x = ∅
14		eueq 1923	. . . . 5 ⊢ (∅ ∈ V ↔ ∃!x x = ∅)
15	13, 14	mpbir 190	. . . 4 ⊢ ∅ ∈ V
16		eleq1 1541	. . . 4 ⊢ ({A} = ∅ → ({A} ∈ V ↔ ∅ ∈ V))
17	15, 16	mpbiri 194	. . 3 ⊢ ({A} = ∅ → {A} ∈ V)
18	8, 17	sylbi 199	. 2 ⊢ (¬ A ∈ V → {A} ∈ V)
19	7, 18	pm2.61i 126	1 ⊢ {A} ∈ V

Syntax hints:  ¬ wn 2  ∀wal 958   = wceq 960   ∈ wcel 962  ∃!weu 1384  Vcvv 1818  ∅c0 2291  ℘cpw 2413  {csn 2421

This theorem is referenced by:  el 2767  snelpw 2768  rext 2770  sspwb 2771  unipw 2772  moabex 2782  nnullss 2784  exss 2785  p0ex 2786  prex 2797  opi1 2800  opth1 2802  opprc3 2813  opth2 2816  opeqsn 2818  opeqpr 2819  opthwiener 2823  uniop 2824  tpex 2894  op1stb 2929  frirr 2940  sucexb 3064  xpsspw 3273  relop 3291  elxp4 3469  elxp5 3470  1stval 4097  2ndval 4098  fo1st 4107  fo2nd 4108  map0 4362  mapsn 4363  ensn1 4442  mapsnen 4447  fiprlem 4451  xpsnen 4454  endisj 4456  xpcomen 4458  xpdom3 4464  fodomr 4502  xpmapenlem2 4517  phplem2 4529  pssnn 4554  abfii2 4577  abfii3 4578  abfii4 4579  fodomfi 4581  pwfilem 4585  elirrv 4613  zfregs 4664  ranksn 4706  rankpr 4709  rankop 4710  ranksuc 4717  aceq5lem2 4753  aceq5lem3 4754  kmlem2 4783  brdom7disj 4821  brdom6disj 4822  unxpdom2 4865  sucxpdom 4866  cfsuc 4935  cdaval 4939  uncdadom 4941  cdaassen 4950  xpcdaen 4951  mapcdaen 4952  cdadom1 4953  exp1 6604  expp1 6605  serz0 7085  serzcmp0i 7087  climconst2 7127  climconst3 7128  climuz0i 7140  climaddc1i 7150  climmulc2i 7161  climsubc2i 7163  climcmpc1i 7171  iserzcmp0i 7175  ser1consti 7203  acdc3lem 7519  acdc2lem2 7522  acdc5lem2 7525  acdclem 7527  ruclem5 7547  infpss 7607  subtop 7674  metelcls 7991  grpsn 8149  ringsn 8188  0ofval 8472  hlim0 9129  hlimcaui 9131  hlimunii 9133  fine 10472  oefil2 10599  cnfilca 10609  1alg 10675  1ded 10692  1cat 10713

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-ext 1464  ax-sep 2718  ax-pow 2758

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 985  df-sb 1176  df-eu 1386  df-mo 1387  df-clab 1470  df-cleq 1475  df-clel 1478  df-ne 1594  df-v 1819  df-dif 2060  df-in 2062  df-ss 2064  df-nul 2292  df-pw 2414  df-sn 2424

Copyright terms: Public domain