Theorem snprc 4742

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1537  ∃wex 1777   ∈ wcel 2108  Vcvv 3488  ∅c0 4352  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-nul 4353  df-sn 4649

This theorem is referenced by:  snnzb  4743  rmosn  4744  rabsnif  4748  prprc1  4790  prprc  4792  preqsnd  4883  unisn2  5330  eqsnuniex  5379  snexALT  5401  snex  5451  posn  5785  frsn  5787  relsnb  5826  relimasn  6114  elimasni  6121  inisegn0  6128  dmsnsnsn  6251  predprc  6370  sucprc  6471  dffv3  6916  fconst5  7243  ordsuci  7844  1stval  8032  2ndval  8033  ecexr  8768  snfi  9109  snfiOLD  9110  domunsn  9193  snnen2oOLD  9290  hashrabrsn  14421  hashrabsn01  14422  hashrabsn1  14423  elprchashprn2  14445  hashsn01  14465  hash2pwpr  14525  snsymgefmndeq  19436  efgrelexlema  19791  usgr1v  29291  1conngr  30226  frgr1v  30303  n0lplig  30515  unidifsnne  32564  eldm3  35723  opelco3  35738  fvsingle  35884  unisnif  35889  funpartlem  35906  bj-sngltag  36949  bj-snex  37001  bj-restsnid  37053  bj-snmooreb  37080  wopprc  42987  safesnsupfidom1o  43379  sn1dom  43488  uneqsn  43987  vsn  48543  mofsn2  48558