Theorem snprc 4656

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 4578	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1855	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4287	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3446	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 304	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 357	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 207   = wceq 1547  ∃wex 1786   ∈ wcel 2119  Vcvv 3432  ∅c0 4268  {csn 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-dif 3893  df-nul 4269  df-sn 4563

This theorem is referenced by:  snnzb  4657  rmosn  4658  rabsnif  4662  prprc1  4704  prprc  4706  preqsnd  4797  unisn2  5241  eqsnuniex  5297  snexALT  5319  snexOLD  5378  posn  5711  frsn  5713  relsnb  5752  relimasn  6044  elimasni  6050  inisegn0  6057  dmsnsnsn  6178  predprc  6296  sucprc  6395  dffv3  6830  fconst5  7157  ordsuci  7758  1stval  7940  2ndval  7941  ecexr  8645  snfi  8987  domunsn  9062  hashrabrsn  14332  hashrabsn01  14333  hashrabsn1  14334  elprchashprn2  14356  hashsn01  14376  hash2pwpr  14436  snsymgefmndeq  19368  efgrelexlema  19722  usgr1v  29350  1conngr  30289  frgr1v  30366  n0lplig  30579  unidifsnne  32631  eldm3  35996  opelco3  36010  fvsingle  36153  unisnif  36158  funpartlem  36177  bj-sngltag  37343  bj-snex  37395  bj-restsnid  37452  bj-snmooreb  37479  wopprc  43482  safesnsupfidom1o  43868  sn1dom  43977  uneqsn  44476  vsn  49309  mofsn2  49342