Theorem snprc 4093

Description: The singleton of a proper class (one that doesn't exist) is the empty set. Theorem 7.2 of [Quine] p. 48. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
snprc

Proof of Theorem snprc

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elsn 4043	. . . 4
2	1	exbii 1667	. . 3
3		neq0 3795	. . 3
4		isset 3113	. . 3
5	2, 3, 4	3bitr4i 277	. 2
6	5	con1bii 331	1

Syntax hints:  -.wn 3  <->wb 184  =wceq 1395  E.wex 1612  e.wcel 1818  cvv 3109  c0 3784  {csn 4029

This theorem is referenced by:  snnzb  4094  rabsnif  4099  prprc1  4140  prprc  4142  unisn2  4588  snexALT  4638  snex  4693  sucprc  4958  posn  5073  frsn  5075  relimasn  5365  elimasni  5369  dmsnsnsn  5491  dffv3  5867  fconst5  6128  1stval  6802  2ndval  6803  ecexr  7335  snfi  7616  domunsn  7687  snnen2o  7726  hashrabrsn  12440  hashrabsn01  12441  hashrabsn1  12442  elprchashprn2  12461  hashsnlei  12478  hash2pwpr  12519  efgrelexlema  16767  usgra1v  24390  cusgra1v  24461  1conngra  24675  eldm3  29191  opelco3  29208  fvsingle  29570  unisnif  29575  funpartlem  29592  wopprc  30972  inisegn0  30989  bj-sngltag  34541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3478  df-nul 3785  df-sn 4030