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 4608	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1848	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4318	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3464	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 303	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 356	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2109  Vcvv 3450  ∅c0 4299  {csn 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-nul 4300  df-sn 4593

This theorem is referenced by:  snnzb  4685  rmosn  4686  rabsnif  4690  prprc1  4732  prprc  4734  preqsnd  4826  unisn2  5270  eqsnuniex  5319  snexALT  5341  snex  5394  posn  5727  frsn  5729  relsnb  5768  relimasn  6059  elimasni  6065  inisegn0  6072  dmsnsnsn  6196  predprc  6314  sucprc  6413  dffv3  6857  fconst5  7183  ordsuci  7787  1stval  7973  2ndval  7974  ecexr  8679  snfi  9017  snfiOLD  9018  domunsn  9097  hashrabrsn  14344  hashrabsn01  14345  hashrabsn1  14346  elprchashprn2  14368  hashsn01  14388  hash2pwpr  14448  snsymgefmndeq  19332  efgrelexlema  19686  usgr1v  29190  1conngr  30130  frgr1v  30207  n0lplig  30419  unidifsnne  32472  eldm3  35755  opelco3  35769  fvsingle  35915  unisnif  35920  funpartlem  35937  bj-sngltag  36978  bj-snex  37030  bj-restsnid  37082  bj-snmooreb  37109  wopprc  43026  safesnsupfidom1o  43413  sn1dom  43522  uneqsn  44021  vsn  48804  mofsn2  48837