Theorem snprc 4726

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 4649	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1843	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4348	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3476	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 302	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 355	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1534  ∃wex 1774   ∈ wcel 2099  Vcvv 3462  ∅c0 4325  {csn 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-dif 3950  df-nul 4326  df-sn 4634

This theorem is referenced by:  snnzb  4727  rmosn  4728  rabsnif  4732  prprc1  4774  prprc  4776  preqsnd  4865  unisn2  5317  eqsnuniex  5365  snexALT  5387  snex  5437  posn  5767  frsn  5769  relsnb  5808  relimasn  6094  elimasni  6101  inisegn0  6108  dmsnsnsn  6231  predprc  6351  sucprc  6452  dffv3  6897  fconst5  7223  ordsuci  7817  1stval  8005  2ndval  8006  ecexr  8739  snfi  9081  snfiOLD  9082  domunsn  9165  snnen2oOLD  9261  hashrabrsn  14389  hashrabsn01  14390  hashrabsn1  14391  elprchashprn2  14413  hashsn01  14433  hash2pwpr  14495  snsymgefmndeq  19392  efgrelexlema  19747  usgr1v  29192  1conngr  30127  frgr1v  30204  n0lplig  30416  unidifsnne  32462  eldm3  35583  opelco3  35598  fvsingle  35744  unisnif  35749  funpartlem  35766  bj-sngltag  36690  bj-snex  36742  bj-restsnid  36794  bj-snmooreb  36821  wopprc  42688  safesnsupfidom1o  43084  sn1dom  43193  uneqsn  43692  vsn  48197  mofsn2  48212