Theorem snprc 4684

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

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1570  ∃wex 1809   ∈ wcel 2143  Vcvv 3455  ∅c0 4287  {csn 4590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3909  df-nul 4288  df-sn 4591

This theorem is referenced by:  snnzb  4685  rmosn  4686  rabsnif  4690  prprc1  4732  prprc  4734  preqsnd  4825  unisn2  5276  eqsnuniex  5334  snexALT  5356  snexOLD  5415  posn  5749  frsn  5751  relsnb  5791  relimasn  6089  elimasni  6095  inisegn0  6102  dmsnsnsn  6223  predprc  6341  sucprc  6441  dffv3  6879  fconst5  7206  ordsuci  7808  1stval  7989  2ndval  7990  ecexr  8700  snfi  9041  domunsn  9116  hashrabrsn  14410  hashrabsn01  14411  hashrabsn1  14412  elprchashprn2  14434  hashsn01  14455  hash2pwpr  14515  snsymgefmndeq  19466  efgrelexlema  19820  usgr1v  29587  1conngr  30526  frgr1v  30603  n0lplig  30816  unidifsnne  32863  eldm3  36234  opelco3  36248  fvsingle  36391  unisnif  36396  funpartlem  36415  bj-sngltag  37600  bj-snex  37652  bj-restsnid  37710  bj-snmooreb  37737  wopprc  43740  safesnsupfidom1o  44126  sn1dom  44235  uneqsn  44734  vsn  49573  mofsn2  49606