Theorem snprc 4680

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 4600	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1881	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4302	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3468	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 306	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 359	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   = wceq 1570  ∃wex 1812   ∈ wcel 2147  Vcvv 3454  ∅c0 4281  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-dif 4050  df-nul 4282  df-sn 4589

This theorem is used by:  snnzb  4681  rmosn  4682  rabsnif  4686  prprc1  4728  prprc  4730  preqsnd  4819  unisn2  5272  eqsnuniex  5330  snexALT  5352  snexOLD  5407  posn  5745  frsn  5747  relsnb  5789  relimasn  6101  elimasni  6107  inisegn0  6114  dmsnsnsn  6240  predprc  6367  sucprc  6467  dffv3  6912  fconst5  7243  ordsuci  7856  1stval  8037  2ndval  8038  ecexr  8760  snfi  9109  domunsn  9184  hashrabrsn  14557  hashrabsn01  14558  hashrabsn1  14559  elprchashprn2  14581  hashsn01  14602  hash2pwpr  14662  snsymgefmndeq  19660  efgrelexlema  20014  usgr1v  29894  1conngr  30852  frgr1v  30929  n0lplig  31142  unidifsnne  33230  eldm3  36741  opelco3  36754  fvsingle  36897  unisnif  36902  funpartlem  36921  bj-sngltag  38111  bj-snex  38163  bj-restsnid  38278  bj-snmooreb  38305  wopprc  44303  safesnsupfidom1o  44679  sn1dom  44788  uneqsn  45286  vsn  50254  mofsn2  50287