Theorem snprc 4253

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 4193	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1774	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 3930	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3207	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 292	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 346	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 196   = wceq 1483  ∃wex 1704   ∈ wcel 1990  Vcvv 3200  ∅c0 3915  {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-nul 3916  df-sn 4178

This theorem is referenced by:  snnzb  4254  rabsnif  4258  prprc1  4300  prprc  4302  unisn2  4794  snexALT  4852  snex  4908  posn  5187  frsn  5189  relimasn  5488  elimasni  5492  inisegn0  5497  dmsnsnsn  5613  sucprc  5800  dffv3  6187  fconst5  6471  1stval  7170  2ndval  7171  ecexr  7747  snfi  8038  domunsn  8110  snnen2o  8149  hashrabrsn  13161  hashrabsn01  13162  hashrabsn1  13163  elprchashprn2  13184  hashsn01  13204  hash2pwpr  13258  efgrelexlema  18162  usgr1v  26148  1conngr  27054  frgr1v  27135  n0lplig  27335  eldm3  31651  opelco3  31678  fvsingle  32027  unisnif  32032  funpartlem  32049  bj-sngltag  32971  bj-restsnid  33040  bj-snmoore  33068  wopprc  37597  uneqsn  38321