Theorem snprc 4678

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 4299	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3465	. . 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 2145  Vcvv 3451  ∅c0 4279  {csn 4584

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-nul 4280  df-sn 4585

This theorem is used by:  snnzb  4679  rmosn  4680  rabsnif  4684  prprc1  4726  prprc  4728  preqsnd  4819  unisn2  5266  eqsnuniex  5323  snexALT  5345  snexOLD  5400  posn  5737  frsn  5739  relsnb  5780  relimasn  6083  elimasni  6089  inisegn0  6096  dmsnsnsn  6220  predprc  6340  sucprc  6440  dffv3  6879  fconst5  7210  ordsuci  7820  1stval  8001  2ndval  8002  ecexr  8715  snfi  9064  domunsn  9139  hashrabrsn  14509  hashrabsn01  14510  hashrabsn1  14511  elprchashprn2  14533  hashsn01  14554  hash2pwpr  14614  snsymgefmndeq  19602  efgrelexlema  19956  usgr1v  29830  1conngr  30788  frgr1v  30865  n0lplig  31078  unidifsnne  33125  eldm3  36505  opelco3  36519  fvsingle  36662  unisnif  36667  funpartlem  36686  bj-sngltag  37876  bj-snex  37928  bj-restsnid  37988  bj-snmooreb  38015  wopprc  44016  safesnsupfidom1o  44402  sn1dom  44511  uneqsn  45010  vsn  49891  mofsn2  49924