Theorem snprc 4673

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 4595	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1867	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4302	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3467	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 305	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 358	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 208   = wceq 1559  ∃wex 1798   ∈ wcel 2141  Vcvv 3453  ∅c0 4283  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-dif 3905  df-nul 4284  df-sn 4580

This theorem is referenced by:  snnzb  4674  rmosn  4675  rabsnif  4679  prprc1  4721  prprc  4723  preqsnd  4814  unisn2  5259  eqsnuniex  5315  snexALT  5337  snexOLD  5396  posn  5729  frsn  5731  relsnb  5771  relimasn  6070  elimasni  6076  inisegn0  6083  dmsnsnsn  6202  predprc  6320  sucprc  6419  dffv3  6858  fconst5  7185  ordsuci  7786  1stval  7967  2ndval  7968  ecexr  8677  snfi  9018  domunsn  9093  hashrabrsn  14379  hashrabsn01  14380  hashrabsn1  14381  elprchashprn2  14403  hashsn01  14423  hash2pwpr  14483  snsymgefmndeq  19426  efgrelexlema  19780  usgr1v  29414  1conngr  30353  frgr1v  30430  n0lplig  30643  unidifsnne  32695  eldm3  36072  opelco3  36086  fvsingle  36229  unisnif  36234  funpartlem  36253  bj-sngltag  37429  bj-snex  37481  bj-restsnid  37538  bj-snmooreb  37565  wopprc  43568  safesnsupfidom1o  43954  sn1dom  44063  uneqsn  44562  vsn  49394  mofsn2  49427