Theorem snex 2740

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

Assertion

Ref	Expression
snex	|- {A} e. V

Proof of Theorem snex

Step	Hyp	Ref	Expression
1		sneq 2407	. . . 4 |- (x = A -> {x} = {A})
2	1	eleq1d 1532	. . 3 |- (x = A -> ({x} e. V <-> {A} e. V))
3		visset 1804	. . . . 5 |- x e. V
4	3	pwex 2735	. . . 4 |- P~x e. V
5		snsspw 2470	. . . 4 |- {x} (_ P~x
6	4, 5	ssexi 2710	. . 3 |- {x} e. V
7	2, 6	vtoclg 1838	. 2 |- (A e. V -> {A} e. V)
8		snprc 2433	. . 3 |- (-. A e. V <-> {A} = (/))
9		axnul 2699	. . . . . . 7 |- E.xA.y -. y e. x
10	9	zfnuleu 2697	. . . . . 6 |- E!xA.y -. y e. x
11		eq0 2284	. . . . . . 7 |- (x = (/) <-> A.y -. y e. x)
12	11	eubii 1380	. . . . . 6 |- (E!x x = (/) <-> E!xA.y -. y e. x)
13	10, 12	mpbir 190	. . . . 5 |- E!x x = (/)
14		eueq 1907	. . . . 5 |- ((/) e. V <-> E!x x = (/))
15	13, 14	mpbir 190	. . . 4 |- (/) e. V
16		eleq1 1526	. . . 4 |- ({A} = (/) -> ({A} e. V <-> (/) e. V))
17	15, 16	mpbiri 194	. . 3 |- ({A} = (/) -> {A} e. V)
18	8, 17	sylbi 199	. 2 |- (-. A e. V -> {A} e. V)
19	7, 18	pm2.61i 126	1 |- {A} e. V

Syntax hints:  -. wn 2  A.wal 951   = wceq 953   e. wcel 955  E!weu 1373  Vcvv 1802  (/)c0 2270  P~cpw 2391  {csn 2399

This theorem is referenced by:  el 2741  snelpw 2742  rext 2744  sspwb 2745  unipw 2746  moabex 2756  nnullss 2758  exss 2759  p0ex 2760  prex 2771  opi1 2774  opth1 2776  opprc3 2787  opth1gOLD 2788  opth2 2789  opeqsn 2791  opeqpr 2792  opthwiener 2796  uniop 2797  tpex 2868  op1stb 2903  frirr 2914  sucexb 3038  xpsspw 3247  relop 3265  elxp4 3439  elxp5 3440  1stval 4065  2ndval 4066  fo1st 4075  fo2nd 4076  map0 4328  mapsn 4329  ensn1 4405  mapsnen 4410  xpsnen 4415  endisj 4417  xpcomen 4419  xpdom3 4425  fodomr 4463  xpmapenlem2 4477  phplem2 4489  pssnn 4513  abfii2 4536  abfii3 4537  abfii4 4538  fodomfi 4540  pwfilem 4544  elirrv 4570  zfregs 4619  ranksn 4661  rankpr 4664  rankop 4665  ranksuc 4672  aceq5lem2 4708  aceq5lem3 4709  kmlem2 4738  brdom7disj 4776  brdom6disj 4777  unxpdom2 4817  sucxpdom 4818  cfsuc 4887  cdavalt 4891  uncdadom 4893  cdaassen 4902  xpcdaen 4903  mapcdaen 4904  cdadom1 4905  exp1t 6505  expp1t 6506  serz0 6991  serzcmp0 6993  climconst2 7032  climconst3 7033  climuz0 7045  climaddc1 7054  climmulc2 7065  climsubc2 7067  climcmpc1 7075  iserzcmp0 7079  ser1const 7107  acdc3lem 7428  acdc2lem2 7431  acdc5lem2 7434  acdclem 7436  ruclem5 7457  subbas 7586  subbas2 7587  subtop 7588  metelcls 7900  grpsn 8061  ringsn 8100  0ofval 8379  hlim0 9026  hlimcau 9028  hlimuni 9030  fine 10348  oefil2 10441  cnfilca 10451  1alg 10498  1ded 10515  1cat 10536

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402

Copyright terms: Public domain