Theorem snprc 4197

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 4141	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1764	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 3889	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3180	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 291	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 345	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 195   = wceq 1475  ∃wex 1695   ∈ wcel 1977  Vcvv 3173  ∅c0 3874  {csn 4125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-nul 3875  df-sn 4126

This theorem is referenced by:  snnzb  4198  rabsnif  4202  prprc1  4243  prprc  4245  unisn2  4722  snexALT  4778  snex  4835  posn  5110  frsn  5112  relimasn  5407  elimasni  5411  inisegn0  5416  dmsnsnsn  5531  sucprc  5717  dffv3  6099  fconst5  6376  1stval  7061  2ndval  7062  ecexr  7634  snfi  7923  domunsn  7995  snnen2o  8034  hashrabrsn  13022  hashrabsn01  13023  hashrabsn1  13024  elprchashprn2  13045  hashsn01  13065  hash2pwpr  13115  efgrelexlema  17985  usgra1v  25919  cusgra1v  25990  1conngra  26203  eldm3  30905  opelco3  30923  fvsingle  31197  unisnif  31202  funpartlem  31219  bj-sngltag  32164  bj-restsnid  32221  wopprc  36615  uneqsn  37341  usgr1v  40482  1conngr  41361  frgr1v  41441