Theorem snex 2750

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

Assertion

Ref	Expression
snex	|- {A} e. V

Proof of Theorem snex

Step	Hyp	Ref	Expression
1		sneq 2417	. . . 4 |- (x = A -> {x} = {A})
2	1	eleq1d 1540	. . 3 |- (x = A -> ({x} e. V <-> {A} e. V))
3		visset 1813	. . . . 5 |- x e. V
4	3	pwex 2745	. . . 4 |- P~x e. V
5		snsspw 2479	. . . 4 |- {x} (_ P~x
6	4, 5	ssexi 2720	. . 3 |- {x} e. V
7	2, 6	vtoclg 1847	. 2 |- (A e. V -> {A} e. V)
8		snprc 2443	. . 3 |- (-. A e. V <-> {A} = (/))
9		axnul 2709	. . . . . . 7 |- E.xA.y -. y e. x
10	9	zfnuleu 2707	. . . . . 6 |- E!xA.y -. y e. x
11		eq0 2294	. . . . . . 7 |- (x = (/) <-> A.y -. y e. x)
12	11	eubii 1387	. . . . . 6 |- (E!x x = (/) <-> E!xA.y -. y e. x)
13	10, 12	mpbir 190	. . . . 5 |- E!x x = (/)
14		eueq 1916	. . . . 5 |- ((/) e. V <-> E!x x = (/))
15	13, 14	mpbir 190	. . . 4 |- (/) e. V
16		eleq1 1534	. . . 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 954   = wceq 956   e. wcel 958  E!weu 1380  Vcvv 1811  (/)c0 2280  P~cpw 2401  {csn 2409

This theorem is referenced by:  el 2751  snelpw 2752  rext 2754  sspwb 2755  unipw 2756  moabex 2766  nnullss 2768  exss 2769  p0ex 2770  prex 2781  opi1 2784  opth1 2786  opprc3 2797  opth2 2800  opeqsn 2802  opeqpr 2803  opthwiener 2807  uniop 2808  tpex 2878  op1stb 2913  frirr 2924  sucexb 3048  xpsspw 3257  relop 3275  elxp4 3453  elxp5 3454  1stval 4081  2ndval 4082  fo1st 4091  fo2nd 4092  map0 4344  mapsn 4345  ensn1 4424  mapsnen 4429  xpsnen 4435  endisj 4437  xpcomen 4439  xpdom3 4445  fodomr 4483  xpmapenlem2 4497  phplem2 4509  pssnn 4534  abfii2OLD 4562  abfii3OLD 4563  abfii4OLD 4564  fodomfiOLD 4566  pwfilemOLD 4570  elirrv 4598  zfregs 4647  ranksn 4689  rankpr 4692  rankop 4693  ranksuc 4700  aceq5lem2 4736  aceq5lem3 4737  kmlem2 4766  brdom7disj 4804  brdom6disj 4805  unxpdom2 4845  sucxpdom 4846  cfsuc 4915  cdavalt 4919  uncdadom 4921  cdaassen 4930  xpcdaen 4931  mapcdaen 4932  cdadom1 4933  exp1t 6573  expp1t 6574  serz0 7053  serzcmp0 7055  climconst2 7095  climconst3 7096  climuz0 7108  climaddc1 7118  climmulc2 7129  climsubc2 7131  climcmpc1 7139  iserzcmp0 7143  ser1const 7171  acdc3lem 7486  acdc2lem2 7489  acdc5lem2 7492  acdclem 7494  ruclem5 7514  infpss 7574  subbasOLD 7644  subbas2OLD 7645  subtop 7646  metelcls 7965  grpsn 8124  ringsn 8163  0ofval 8447  hlim0 9105  hlimcau 9107  hlimuni 9109  fine 10449  fineOLD 10450  oefil2 10567  cnfilca 10583  cnfilcaOLD 10584  1alg 10654  1ded 10671  1cat 10692

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412

Copyright terms: Public domain