Theorem snprc 2447

Description: The singleton of a proper class (one that doesn't exist) is the empty set. Theorem 7.2 of [Quine] p. 48.

Assertion

Ref	Expression
snprc	|- (-. A e. V <-> {A} = (/))

Proof of Theorem snprc

Step	Hyp	Ref	Expression
1		elsn 2425	. . . 4 |- (x e. {A} <-> x = A)
2	1	exbii 1053	. . 3 |- (E.x x e. {A} <-> E.x x = A)
3		n0 2293	. . 3 |- (-. {A} = (/) <-> E.x x e. {A})
4		isset 1817	. . 3 |- (A e. V <-> E.x x = A)
5	2, 3, 4	3bitr4 183	. 2 |- (-. {A} = (/) <-> A e. V)
6	5	con1bii 220	1 |- (-. A e. V <-> {A} = (/))

Syntax hints:  -. wn 2   <-> wb 146   = wceq 958   e. wcel 960  E.wex 982  Vcvv 1814  (/)c0 2283  {csn 2413

This theorem is referenced by:  prprc1 2456  prprc 2458  snsspr 2474  opprc1 2502  snex 2756  opprc3 2803  unisn2 2881  sucprc 3050  dmsnop 3334  relimasn 3431  fvprc 3727  fconst5 3854  1stval 4087  2ndval 4088  snfi 4438  snfiOLD 4439

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-v 1815  df-dif 2052  df-nul 2284  df-sn 2416

Copyright terms: Public domain