NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  snid GIF version

Theorem snid 3760
Description: A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 31-Dec-1993.)
Hypothesis
Ref Expression
snid.1 A V
Assertion
Ref Expression
snid A {A}

Proof of Theorem snid
StepHypRef Expression
1 snid.1 . 2 A V
2 snidb 3759 . 2 (A V ↔ A {A})
31, 2mpbi 199 1 A {A}
Colors of variables: wff setvar class
Syntax hints:   wcel 1710  Vcvv 2859  {csn 3737
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861  df-sn 3741
This theorem is referenced by:  rabsnt  3797  sneqr  3872  unsneqsn  3887  unipw  4117  eqpw1uni  4330  pw1eqadj  4332  0nelsuc  4400  0cnsuc  4401  nnsucelr  4428  nndisjeq  4429  ssfin  4470  eqtfinrelk  4486  0ceven  4505  vfinspss  4551  proj1op  4600  proj2op  4601  fsn  5432  fsn2  5434  fnressn  5438  fressnfv  5439  fvsn  5445  fvsnun1  5447  dmep  5524  map0  6025  mapsn  6026  xpsnen  6049  enadj  6060  2p1e3c  6156  frecxp  6314
  Copyright terms: Public domain W3C validator