Theorem snprc 4678

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	⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Proof of Theorem snprc

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		velsn 4600	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1881	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4299	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3464	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 306	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 359	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   = wceq 1570  ∃wex 1812   ∈ wcel 2145  Vcvv 3450  ∅c0 4279  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-nul 4280  df-sn 4585

This theorem is used by:  snnzb  4679  rmosn  4680  rabsnif  4684  prprc1  4726  prprc  4728  preqsnd  4819  unisn2  5269  eqsnuniex  5326  snexALT  5348  snexOLD  5407  posn  5741  frsn  5743  relsnb  5783  relimasn  6081  elimasni  6087  inisegn0  6094  dmsnsnsn  6216  predprc  6336  sucprc  6436  dffv3  6874  fconst5  7205  ordsuci  7807  1stval  7988  2ndval  7989  ecexr  8701  snfi  9050  domunsn  9125  hashrabrsn  14436  hashrabsn01  14437  hashrabsn1  14438  elprchashprn2  14460  hashsn01  14481  hash2pwpr  14541  snsymgefmndeq  19522  efgrelexlema  19876  usgr1v  29716  1conngr  30674  frgr1v  30751  n0lplig  30964  unidifsnne  33011  eldm3  36340  opelco3  36354  fvsingle  36497  unisnif  36502  funpartlem  36521  bj-sngltag  37727  bj-snex  37779  bj-restsnid  37837  bj-snmooreb  37864  wopprc  43871  safesnsupfidom1o  44257  sn1dom  44366  uneqsn  44865  vsn  49740  mofsn2  49773