Theorem snprc 4674

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 4596	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1880	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4298	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3464	. . 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 1569  ∃wex 1811   ∈ wcel 2144  Vcvv 3450  ∅c0 4278  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 4047  df-nul 4279  df-sn 4585

This theorem is used by:  snnzb  4675  rmosn  4676  rabsnif  4680  prprc1  4722  prprc  4724  preqsnd  4813  unisn2  5265  eqsnuniex  5322  snexALT  5344  snexOLD  5399  posn  5736  frsn  5738  relsnb  5779  relimasn  6082  elimasni  6088  inisegn0  6095  dmsnsnsn  6221  predprc  6341  sucprc  6441  dffv3  6882  fconst5  7213  ordsuci  7823  1stval  8004  2ndval  8005  ecexr  8726  snfi  9075  domunsn  9150  hashrabrsn  14520  hashrabsn01  14521  hashrabsn1  14522  elprchashprn2  14544  hashsn01  14565  hash2pwpr  14625  snsymgefmndeq  19615  efgrelexlema  19969  usgr1v  29843  1conngr  30801  frgr1v  30878  n0lplig  31091  unidifsnne  33180  eldm3  36619  opelco3  36632  fvsingle  36775  unisnif  36780  funpartlem  36799  bj-sngltag  37989  bj-snex  38041  bj-restsnid  38101  bj-snmooreb  38128  wopprc  44131  safesnsupfidom1o  44512  sn1dom  44621  uneqsn  45119  vsn  50017  mofsn2  50050