Theorem snex 2718

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

Assertion

Ref	Expression
snex	|- {A} e. V

Proof of Theorem snex

Step	Hyp	Ref	Expression
1		sneq 2388	. . . 4 |- (x = A -> {x} = {A})
2	1	eleq1d 1516	. . 3 |- (x = A -> ({x} e. V <-> {A} e. V))
3		visset 1788	. . . . 5 |- x e. V
4	3	pwex 2713	. . . 4 |- P~x e. V
5		snsspw 2449	. . . 4 |- {x} (_ P~x
6	4, 5	ssexi 2688	. . 3 |- {x} e. V
7	2, 6	vtoclg 1822	. 2 |- (A e. V -> {A} e. V)
8		snprc 2414	. . 3 |- (-. A e. V <-> {A} = (/))
9		axnul 2677	. . . . . . 7 |- E.xA.y -. y e. x
10	9	zfnuleu 2675	. . . . . 6 |- E!xA.y -. y e. x
11		eq0 2265	. . . . . . 7 |- (x = (/) <-> A.y -. y e. x)
12	11	eubii 1364	. . . . . 6 |- (E!x x = (/) <-> E!xA.y -. y e. x)
13	10, 12	mpbir 190	. . . . 5 |- E!x x = (/)
14		eueq 1888	. . . . 5 |- ((/) e. V <-> E!x x = (/))
15	13, 14	mpbir 190	. . . 4 |- (/) e. V
16		eleq1 1510	. . . 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 950   = wceq 1099   e. wcel 1105  E!weu 1357  Vcvv 1786  (/)c0 2251  P~cpw 2372  {csn 2380

This theorem is referenced by:  el 2719  snelpw 2720  rext 2722  sspwb 2723  unipw 2724  moabex 2734  nnullss 2736  exss 2737  p0ex 2738  prex 2749  opi1 2752  opth 2754  opprc3 2764  opth2 2765  opthwiener 2770  uniop 2771  tpex 2841  op1stb 2876  frirr 2887  sucexb 3011  xpsspw 3219  elxp4 3402  elxp5 3403  1stval 4019  2ndval 4020  fo1st 4029  fo2nd 4030  map0 4282  mapsn 4283  ensn1 4359  mapsnen 4364  xpsnen 4369  endisj 4371  xpcomen 4373  xpdom3 4379  fodomr 4417  xpmapenlem2 4429  phplem2 4441  pssnn 4465  abfii2 4488  abfii3 4489  abfii4 4490  fodomfi 4492  pwfilem 4496  elirrv 4522  zfregs 4571  ranksn 4613  rankpr 4616  rankop 4617  ranksuc 4624  aceq5lem2 4660  aceq5lem3 4661  kmlem2 4690  brdom7disj 4728  brdom6disj 4729  cardsn 4757  unxpdom2 4768  sucxpdom 4769  cfsuc 4838  cdavalt 4842  uncdadom 4844  cdaassen 4853  xpcdaen 4854  mapcdaen 4855  cdadom1 4856  exp1t 6456  expp1t 6457  serz0 6942  serzcmp0 6944  climconst2 6983  climconst3 6984  climuz0 6996  climaddc1 7005  climmulc2 7016  climsubc2 7018  climcmpc1 7026  iserzcmp0 7030  ser1const 7058  acdc3lem 7379  acdc2lem2 7382  acdc5lem2 7385  acdclem 7387  ruclem5 7408  subbas 7537  subbas2 7538  subtop 7539  metelcls 7848  grpsn 8009  ringsn 8048  0ofval 8314  fine 8707  oefil2 8791  cnfilca 8801  1alg 8848  1ded 8865  1cat 8886  hlim0 9256  hlimcau 9258  hlimuni 9260

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-sep 2671  ax-pow 2710

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-v 1787  df-dif 2020  df-in 2022  df-ss 2024  df-nul 2252  df-pw 2373  df-sn 2383

Copyright terms: Public domain