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.

Step	Hyp	Ref	Expression
1		velsn 4342	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1927	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4088	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3364	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 293	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 346	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

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