Theorem snprc 4681

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2109  Vcvv 3447  ∅c0 4296  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-nul 4297  df-sn 4590

This theorem is referenced by:  snnzb  4682  rmosn  4683  rabsnif  4687  prprc1  4729  prprc  4731  preqsnd  4823  unisn2  5267  eqsnuniex  5316  snexALT  5338  snex  5391  posn  5724  frsn  5726  relsnb  5765  relimasn  6056  elimasni  6062  inisegn0  6069  dmsnsnsn  6193  predprc  6311  sucprc  6410  dffv3  6854  fconst5  7180  ordsuci  7784  1stval  7970  2ndval  7971  ecexr  8676  snfi  9014  snfiOLD  9015  domunsn  9091  hashrabrsn  14337  hashrabsn01  14338  hashrabsn1  14339  elprchashprn2  14361  hashsn01  14381  hash2pwpr  14441  snsymgefmndeq  19325  efgrelexlema  19679  usgr1v  29183  1conngr  30123  frgr1v  30200  n0lplig  30412  unidifsnne  32465  eldm3  35748  opelco3  35762  fvsingle  35908  unisnif  35913  funpartlem  35930  bj-sngltag  36971  bj-snex  37023  bj-restsnid  37075  bj-snmooreb  37102  wopprc  43019  safesnsupfidom1o  43406  sn1dom  43515  uneqsn  44014  vsn  48800  mofsn2  48833