Theorem snprc 4670

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 4592	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1849	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4302	. . 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 1541  ∃wex 1780   ∈ wcel 2111  Vcvv 3436  ∅c0 4283  {csn 4576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3905  df-nul 4284  df-sn 4577

This theorem is referenced by:  snnzb  4671  rmosn  4672  rabsnif  4676  prprc1  4718  prprc  4720  preqsnd  4811  unisn2  5250  eqsnuniex  5299  snexALT  5321  snex  5374  posn  5702  frsn  5704  relsnb  5742  relimasn  6034  elimasni  6040  inisegn0  6047  dmsnsnsn  6167  predprc  6285  sucprc  6384  dffv3  6818  fconst5  7140  ordsuci  7741  1stval  7923  2ndval  7924  ecexr  8627  snfi  8965  domunsn  9040  hashrabrsn  14279  hashrabsn01  14280  hashrabsn1  14281  elprchashprn2  14303  hashsn01  14323  hash2pwpr  14383  snsymgefmndeq  19308  efgrelexlema  19662  usgr1v  29235  1conngr  30172  frgr1v  30249  n0lplig  30461  unidifsnne  32514  eldm3  35803  opelco3  35817  fvsingle  35960  unisnif  35965  funpartlem  35982  bj-sngltag  37023  bj-snex  37075  bj-restsnid  37127  bj-snmooreb  37154  wopprc  43069  safesnsupfidom1o  43456  sn1dom  43565  uneqsn  44064  vsn  48849  mofsn2  48882