Theorem snprc 4720

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 4643	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1850	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4344	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3487	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 302	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 356	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1541  ∃wex 1781   ∈ wcel 2106  Vcvv 3474  ∅c0 4321  {csn 4627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3950  df-nul 4322  df-sn 4628

This theorem is referenced by:  snnzb  4721  rmosn  4722  rabsnif  4726  prprc1  4768  prprc  4770  preqsnd  4858  unisn2  5311  eqsnuniex  5358  snexALT  5380  snex  5430  posn  5759  frsn  5761  relsnb  5800  relimasn  6080  elimasni  6087  inisegn0  6094  dmsnsnsn  6216  predprc  6336  sucprc  6437  dffv3  6884  fconst5  7203  ordsuci  7792  1stval  7973  2ndval  7974  ecexr  8704  snfi  9040  domunsn  9123  snnen2oOLD  9223  hashrabrsn  14328  hashrabsn01  14329  hashrabsn1  14330  elprchashprn2  14352  hashsn01  14372  hash2pwpr  14433  snsymgefmndeq  19256  efgrelexlema  19611  usgr1v  28502  1conngr  29436  frgr1v  29513  n0lplig  29723  unidifsnne  31760  eldm3  34719  opelco3  34734  fvsingle  34880  unisnif  34885  funpartlem  34902  bj-sngltag  35852  bj-snex  35904  bj-restsnid  35956  bj-snmooreb  35983  wopprc  41754  safesnsupfidom1o  42153  sn1dom  42262  uneqsn  42761  vsn  47449  mofsn2  47464