Theorem snprc 4685

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 4607	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1881	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4306	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3471	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 306	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 359	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   = wceq 1570  ∃wex 1812   ∈ wcel 2146  Vcvv 3457  ∅c0 4286  {csn 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-nul 4287  df-sn 4592

This theorem is used by:  snnzb  4686  rmosn  4687  rabsnif  4691  prprc1  4733  prprc  4735  preqsnd  4826  unisn2  5277  eqsnuniex  5334  snexALT  5356  snexOLD  5415  posn  5749  frsn  5751  relsnb  5791  relimasn  6089  elimasni  6095  inisegn0  6102  dmsnsnsn  6223  predprc  6343  sucprc  6443  dffv3  6881  fconst5  7208  ordsuci  7809  1stval  7990  2ndval  7991  ecexr  8701  snfi  9043  domunsn  9118  hashrabrsn  14421  hashrabsn01  14422  hashrabsn1  14423  elprchashprn2  14445  hashsn01  14466  hash2pwpr  14526  snsymgefmndeq  19488  efgrelexlema  19842  usgr1v  29635  1conngr  30574  frgr1v  30651  n0lplig  30864  unidifsnne  32911  eldm3  36266  opelco3  36280  fvsingle  36423  unisnif  36428  funpartlem  36447  bj-sngltag  37652  bj-snex  37704  bj-restsnid  37762  bj-snmooreb  37789  wopprc  43790  safesnsupfidom1o  44176  sn1dom  44285  uneqsn  44784  vsn  49623  mofsn2  49656