Theorem snprc 4408

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 4350	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1943	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4094	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3360	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 294	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 347	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 197   = wceq 1652  ∃wex 1874   ∈ wcel 2155  Vcvv 3350  ∅c0 4079  {csn 4334

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-dif 3735  df-nul 4080  df-sn 4335

This theorem is referenced by:  snnzb  4409  rabsnif  4413  prprc1  4455  prprc  4457  preqsnd  4543  unisn2  4955  snexALT  5018  snex  5064  posn  5357  frsn  5359  relimasn  5670  elimasni  5674  inisegn0  5679  dmsnsnsn  5797  sucprc  5983  dffv3  6371  fconst5  6664  1stval  7368  2ndval  7369  ecexr  7952  snfi  8245  domunsn  8317  snnen2o  8356  hashrabrsn  13363  hashrabsn01  13364  hashrabsn1  13365  elprchashprn2  13385  hashsn01  13405  hash2pwpr  13459  efgrelexlema  18428  usgr1v  26427  1conngr  27430  frgr1v  27509  n0lplig  27729  eldm3  32028  opelco3  32053  fvsingle  32403  unisnif  32408  funpartlem  32425  bj-sngltag  33330  bj-restsnid  33400  bj-snmoore  33428  wopprc  38206  uneqsn  38927