MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snprc Structured version   Visualization version   GIF version

Theorem snprc 4400
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.
StepHypRef Expression
1 velsn 4342 . . . 4 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
21exbii 1927 . . 3 (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3 neq0 4088 . . 3 (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4 isset 3364 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
52, 3, 43bitr4i 293 . 2 (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
65con1bii 346 1 𝐴 ∈ V ↔ {𝐴} = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 197   = wceq 1634  wex 1855  wcel 2148  Vcvv 3355  c0 4073  {csn 4326
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-v 3357  df-dif 3732  df-nul 4074  df-sn 4327
This theorem is referenced by:  snnzb  4401  rabsnif  4405  prprc1  4447  prprc  4449  preqsnd  4534  unisn2  4942  snexALT  4997  snex  5050  posn  5339  frsn  5341  relimasn  5639  elimasni  5643  inisegn0  5648  dmsnsnsn  5766  sucprc  5954  dffv3  6344  fconst5  6634  1stval  7338  2ndval  7339  ecexr  7922  snfi  8215  domunsn  8287  snnen2o  8326  hashrabrsn  13385  hashrabsn01  13386  hashrabsn1  13387  elprchashprn2  13408  hashsn01  13428  hash2pwpr  13482  efgrelexlema  18389  usgr1v  26392  1conngr  27395  frgr1v  27474  n0lplig  27694  eldm3  32006  opelco3  32031  fvsingle  32381  unisnif  32386  funpartlem  32403  bj-sngltag  33319  bj-restsnid  33389  bj-snmoore  33417  wopprc  38138  uneqsn  38861
  Copyright terms: Public domain W3C validator