Theorem snprc 4671

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1541  ∃wex 1780   ∈ wcel 2113  Vcvv 3437  ∅c0 4282  {csn 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901  df-nul 4283  df-sn 4578

This theorem is referenced by:  snnzb  4672  rmosn  4673  rabsnif  4677  prprc1  4719  prprc  4721  preqsnd  4812  unisn2  5254  eqsnuniex  5303  snexALT  5325  snex  5378  posn  5707  frsn  5709  relsnb  5748  relimasn  6041  elimasni  6047  inisegn0  6054  dmsnsnsn  6175  predprc  6293  sucprc  6392  dffv3  6827  fconst5  7149  ordsuci  7750  1stval  7932  2ndval  7933  ecexr  8636  snfi  8976  domunsn  9051  hashrabrsn  14286  hashrabsn01  14287  hashrabsn1  14288  elprchashprn2  14310  hashsn01  14330  hash2pwpr  14390  snsymgefmndeq  19315  efgrelexlema  19669  usgr1v  29255  1conngr  30195  frgr1v  30272  n0lplig  30484  unidifsnne  32537  eldm3  35877  opelco3  35891  fvsingle  36034  unisnif  36039  funpartlem  36058  bj-sngltag  37100  bj-snex  37152  bj-restsnid  37204  bj-snmooreb  37231  wopprc  43187  safesnsupfidom1o  43574  sn1dom  43683  uneqsn  44182  vsn  48973  mofsn2  49006