Theorem snprc 4610

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 4538	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1849	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4244	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3422	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 306	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 360	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1538  ∃wex 1781   ∈ wcel 2111  Vcvv 3409  ∅c0 4225  {csn 4522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-fal 1551  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-dif 3861  df-nul 4226  df-sn 4523

This theorem is referenced by:  snnzb  4611  rmosn  4612  rabsnif  4616  prprc1  4658  prprc  4660  preqsnd  4746  unisn2  5182  snexALT  5252  snex  5300  posn  5606  frsn  5608  relsnb  5644  relimasn  5924  elimasni  5928  inisegn0  5933  dmsnsnsn  6049  sucprc  6244  dffv3  6654  fconst5  6959  1stval  7695  2ndval  7696  ecexr  8304  snfi  8614  domunsn  8689  snnen2o  8729  hashrabrsn  13783  hashrabsn01  13784  hashrabsn1  13785  elprchashprn2  13807  hashsn01  13827  hash2pwpr  13886  snsymgefmndeq  18590  efgrelexlema  18942  usgr1v  27145  1conngr  28078  frgr1v  28155  n0lplig  28365  unidifsnne  30406  eldm3  33244  opelco3  33265  fvsingle  33771  unisnif  33776  funpartlem  33793  bj-sngltag  34700  bj-restsnid  34782  bj-snmooreb  34809  wopprc  40344  sn1dom  40607  uneqsn  41099