Theorem snprc 4722

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 4645	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1851	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4346	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3488	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 303	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 357	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1542  ∃wex 1782   ∈ wcel 2107  Vcvv 3475  ∅c0 4323  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-nul 4324  df-sn 4630

This theorem is referenced by:  snnzb  4723  rmosn  4724  rabsnif  4728  prprc1  4770  prprc  4772  preqsnd  4860  unisn2  5313  eqsnuniex  5360  snexALT  5382  snex  5432  posn  5762  frsn  5764  relsnb  5803  relimasn  6084  elimasni  6091  inisegn0  6098  dmsnsnsn  6220  predprc  6340  sucprc  6441  dffv3  6888  fconst5  7207  ordsuci  7796  1stval  7977  2ndval  7978  ecexr  8708  snfi  9044  domunsn  9127  snnen2oOLD  9227  hashrabrsn  14332  hashrabsn01  14333  hashrabsn1  14334  elprchashprn2  14356  hashsn01  14376  hash2pwpr  14437  snsymgefmndeq  19262  efgrelexlema  19617  usgr1v  28513  1conngr  29447  frgr1v  29524  n0lplig  29736  unidifsnne  31773  eldm3  34731  opelco3  34746  fvsingle  34892  unisnif  34897  funpartlem  34914  bj-sngltag  35864  bj-snex  35916  bj-restsnid  35968  bj-snmooreb  35995  wopprc  41769  safesnsupfidom1o  42168  sn1dom  42277  uneqsn  42776  vsn  47496  mofsn2  47511