Theorem snex 2746

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 2773, Replacement is not needed.

Assertion

Ref	Expression
snex	⊢ {A} ∈ V

Proof of Theorem snex

Step	Hyp	Ref	Expression
1		sneq 2414	. . . 4 ⊢ (x = A → {x} = {A})
2	1	eleq1d 1538	. . 3 ⊢ (x = A → ({x} ∈ V ↔ {A} ∈ V))
3		visset 1810	. . . . 5 ⊢ x ∈ V
4	3	pwex 2741	. . . 4 ⊢ ℘x ∈ V
5		snsspw 2476	. . . 4 ⊢ {x} ⊆ ℘x
6	4, 5	ssexi 2716	. . 3 ⊢ {x} ∈ V
7	2, 6	vtoclg 1844	. 2 ⊢ (A ∈ V → {A} ∈ V)
8		snprc 2440	. . 3 ⊢ (¬ A ∈ V ↔ {A} = ∅)
9		axnul 2705	. . . . . . 7 ⊢ ∃x∀y ¬ y ∈ x
10	9	zfnuleu 2703	. . . . . 6 ⊢ ∃!x∀y ¬ y ∈ x
11		eq0 2291	. . . . . . 7 ⊢ (x = ∅ ↔ ∀y ¬ y ∈ x)
12	11	eubii 1386	. . . . . 6 ⊢ (∃!x x = ∅ ↔ ∃!x∀y ¬ y ∈ x)
13	10, 12	mpbir 190	. . . . 5 ⊢ ∃!x x = ∅
14		eueq 1913	. . . . 5 ⊢ (∅ ∈ V ↔ ∃!x x = ∅)
15	13, 14	mpbir 190	. . . 4 ⊢ ∅ ∈ V
16		eleq1 1532	. . . 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 953   = wceq 955   ∈ wcel 957  ∃!weu 1379  Vcvv 1808  ∅c0 2277  ℘cpw 2398  {csn 2406

This theorem is referenced by:  el 2747  snelpw 2748  rext 2750  sspwb 2751  unipw 2752  moabex 2762  nnullss 2764  exss 2765  p0ex 2766  prex 2777  opi1 2780  opth1 2782  opprc3 2793  opth2 2796  opeqsn 2798  opeqpr 2799  opthwiener 2803  uniop 2804  tpex 2874  op1stb 2909  frirr 2920  sucexb 3044  xpsspw 3253  relop 3271  elxp4 3449  elxp5 3450  1stval 4074  2ndval 4075  fo1st 4084  fo2nd 4085  map0 4337  mapsn 4338  ensn1 4414  mapsnen 4419  xpsnen 4424  endisj 4426  xpcomen 4428  xpdom3 4434  fodomr 4472  xpmapenlem2 4486  phplem2 4498  pssnn 4522  abfii2 4545  abfii3 4546  abfii4 4547  fodomfi 4549  pwfilem 4553  elirrv 4581  zfregs 4630  ranksn 4672  rankpr 4675  rankop 4676  ranksuc 4683  aceq5lem2 4719  aceq5lem3 4720  kmlem2 4749  brdom7disj 4787  brdom6disj 4788  unxpdom2 4828  sucxpdom 4829  cfsuc 4898  cdavalt 4902  uncdadom 4904  cdaassen 4913  xpcdaen 4914  mapcdaen 4915  cdadom1 4916  exp1t 6518  expp1t 6519  serz0 7006  serzcmp0 7008  climconst2 7048  climconst3 7049  climuz0 7061  climaddc1 7071  climmulc2 7082  climsubc2 7084  climcmpc1 7092  iserzcmp0 7096  ser1const 7124  acdc3lem 7445  acdc2lem2 7448  acdc5lem2 7451  acdclem 7453  ruclem5 7474  infpss 7534  subbas 7604  subbas2 7605  subtop 7606  metelcls 7927  grpsn 8088  ringsn 8127  0ofval 8407  hlim0 9060  hlimcau 9062  hlimuni 9064  fine 10406  oefil2 10500  cnfilca 10510  1alg 10570  1ded 10587  1cat 10608

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-sep 2699  ax-pow 2738

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-v 1809  df-dif 2046  df-in 2048  df-ss 2050  df-nul 2278  df-pw 2399  df-sn 2409

Copyright terms: Public domain