Theorem snprc 4650

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 4574	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1851	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4276	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3435	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 302	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 356	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1539  ∃wex 1783   ∈ wcel 2108  Vcvv 3422  ∅c0 4253  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-nul 4254  df-sn 4559

This theorem is referenced by:  snnzb  4651  rmosn  4652  rabsnif  4656  prprc1  4698  prprc  4700  preqsnd  4786  unisn2  5231  eqsnuniex  5278  snexALT  5301  snex  5349  posn  5663  frsn  5665  relsnb  5701  relimasn  5981  elimasni  5988  inisegn0  5995  dmsnsnsn  6112  sucprc  6326  dffv3  6752  fconst5  7063  1stval  7806  2ndval  7807  ecexr  8461  snfi  8788  domunsn  8863  snnen2o  8903  hashrabrsn  14015  hashrabsn01  14016  hashrabsn1  14017  elprchashprn2  14039  hashsn01  14059  hash2pwpr  14118  snsymgefmndeq  18917  efgrelexlema  19270  usgr1v  27526  1conngr  28459  frgr1v  28536  n0lplig  28746  unidifsnne  30785  eldm3  33634  opelco3  33655  fvsingle  34149  unisnif  34154  funpartlem  34171  bj-sngltag  35100  bj-restsnid  35185  bj-snmooreb  35212  wopprc  40768  sn1dom  41031  uneqsn  41522  vsn  46045  mofsn2  46060