Theorem snprc 4653

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 4577	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1850	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4279	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3445	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 303	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 357	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1539  ∃wex 1782   ∈ wcel 2106  Vcvv 3432  ∅c0 4256  {csn 4561

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-nul 4257  df-sn 4562

This theorem is referenced by:  snnzb  4654  rmosn  4655  rabsnif  4659  prprc1  4701  prprc  4703  preqsnd  4789  unisn2  5236  eqsnuniex  5283  snexALT  5306  snex  5354  posn  5672  frsn  5674  relsnb  5712  relimasn  5992  elimasni  5999  inisegn0  6006  dmsnsnsn  6123  predprc  6241  sucprc  6341  dffv3  6770  fconst5  7081  1stval  7833  2ndval  7834  ecexr  8503  snfi  8834  domunsn  8914  snnen2oOLD  9010  hashrabrsn  14087  hashrabsn01  14088  hashrabsn1  14089  elprchashprn2  14111  hashsn01  14131  hash2pwpr  14190  snsymgefmndeq  19002  efgrelexlema  19355  usgr1v  27623  1conngr  28558  frgr1v  28635  n0lplig  28845  unidifsnne  30884  eldm3  33728  opelco3  33749  fvsingle  34222  unisnif  34227  funpartlem  34244  bj-sngltag  35173  bj-restsnid  35258  bj-snmooreb  35285  wopprc  40852  sn1dom  41133  uneqsn  41633  vsn  46157  mofsn2  46172