Theorem snprc 4671

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 4595	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1848	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4305	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3452	. . 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 3438  ∅c0 4286  {csn 4579

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-dif 3908  df-nul 4287  df-sn 4580

This theorem is referenced by:  snnzb  4672  rmosn  4673  rabsnif  4677  prprc1  4719  prprc  4721  preqsnd  4813  unisn2  5254  eqsnuniex  5303  snexALT  5325  snex  5378  posn  5709  frsn  5711  relsnb  5749  relimasn  6040  elimasni  6046  inisegn0  6053  dmsnsnsn  6173  predprc  6290  sucprc  6389  dffv3  6822  fconst5  7146  ordsuci  7748  1stval  7933  2ndval  7934  ecexr  8637  snfi  8975  snfiOLD  8976  domunsn  9051  hashrabrsn  14297  hashrabsn01  14298  hashrabsn1  14299  elprchashprn2  14321  hashsn01  14341  hash2pwpr  14401  snsymgefmndeq  19292  efgrelexlema  19646  usgr1v  29219  1conngr  30156  frgr1v  30233  n0lplig  30445  unidifsnne  32498  eldm3  35736  opelco3  35750  fvsingle  35896  unisnif  35901  funpartlem  35918  bj-sngltag  36959  bj-snex  37011  bj-restsnid  37063  bj-snmooreb  37090  wopprc  43006  safesnsupfidom1o  43393  sn1dom  43502  uneqsn  44001  vsn  48800  mofsn2  48833