Theorem snprc 4669

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 4593	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1848	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4303	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3450	. . 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 3436  ∅c0 4284  {csn 4577

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 3438  df-dif 3906  df-nul 4285  df-sn 4578

This theorem is referenced by:  snnzb  4670  rmosn  4671  rabsnif  4675  prprc1  4717  prprc  4719  preqsnd  4810  unisn2  5251  eqsnuniex  5300  snexALT  5322  snex  5375  posn  5705  frsn  5707  relsnb  5745  relimasn  6036  elimasni  6042  inisegn0  6049  dmsnsnsn  6169  predprc  6286  sucprc  6385  dffv3  6818  fconst5  7142  ordsuci  7744  1stval  7926  2ndval  7927  ecexr  8630  snfi  8968  snfiOLD  8969  domunsn  9044  hashrabrsn  14279  hashrabsn01  14280  hashrabsn1  14281  elprchashprn2  14303  hashsn01  14323  hash2pwpr  14383  snsymgefmndeq  19274  efgrelexlema  19628  usgr1v  29201  1conngr  30138  frgr1v  30215  n0lplig  30427  unidifsnne  32480  eldm3  35738  opelco3  35752  fvsingle  35898  unisnif  35903  funpartlem  35920  bj-sngltag  36961  bj-snex  37013  bj-restsnid  37065  bj-snmooreb  37092  wopprc  43007  safesnsupfidom1o  43394  sn1dom  43503  uneqsn  44002  vsn  48800  mofsn2  48833