Theorem snprc 4721

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 4646	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1844	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4357	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3491	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 303	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 356	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1536  ∃wex 1775   ∈ wcel 2105  Vcvv 3477  ∅c0 4338  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-nul 4339  df-sn 4631

This theorem is referenced by:  snnzb  4722  rmosn  4723  rabsnif  4727  prprc1  4769  prprc  4771  preqsnd  4863  unisn2  5317  eqsnuniex  5366  snexALT  5388  snex  5441  posn  5773  frsn  5775  relsnb  5814  relimasn  6104  elimasni  6111  inisegn0  6118  dmsnsnsn  6241  predprc  6360  sucprc  6461  dffv3  6902  fconst5  7225  ordsuci  7827  1stval  8014  2ndval  8015  ecexr  8748  snfi  9081  snfiOLD  9082  domunsn  9165  snnen2oOLD  9261  hashrabrsn  14407  hashrabsn01  14408  hashrabsn1  14409  elprchashprn2  14431  hashsn01  14451  hash2pwpr  14511  snsymgefmndeq  19426  efgrelexlema  19781  usgr1v  29287  1conngr  30222  frgr1v  30299  n0lplig  30511  unidifsnne  32561  eldm3  35740  opelco3  35755  fvsingle  35901  unisnif  35906  funpartlem  35923  bj-sngltag  36965  bj-snex  37017  bj-restsnid  37069  bj-snmooreb  37096  wopprc  43018  safesnsupfidom1o  43406  sn1dom  43515  uneqsn  44014  vsn  48659  mofsn2  48674