Theorem snprc 4676

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3442  ∅c0 4287  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-nul 4288  df-sn 4583

This theorem is referenced by:  snnzb  4677  rmosn  4678  rabsnif  4682  prprc1  4724  prprc  4726  preqsnd  4817  unisn2  5259  eqsnuniex  5308  snexALT  5330  snexOLD  5388  posn  5718  frsn  5720  relsnb  5759  relimasn  6052  elimasni  6058  inisegn0  6065  dmsnsnsn  6186  predprc  6304  sucprc  6403  dffv3  6838  fconst5  7162  ordsuci  7763  1stval  7945  2ndval  7946  ecexr  8650  snfi  8992  domunsn  9067  hashrabrsn  14307  hashrabsn01  14308  hashrabsn1  14309  elprchashprn2  14331  hashsn01  14351  hash2pwpr  14411  snsymgefmndeq  19336  efgrelexlema  19690  usgr1v  29341  1conngr  30281  frgr1v  30358  n0lplig  30570  unidifsnne  32622  eldm3  35974  opelco3  35988  fvsingle  36131  unisnif  36136  funpartlem  36155  bj-sngltag  37228  bj-snex  37280  bj-restsnid  37337  bj-snmooreb  37364  wopprc  43384  safesnsupfidom1o  43770  sn1dom  43879  uneqsn  44378  vsn  49168  mofsn2  49201