MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snid Structured version   Visualization version   Unicode version

Theorem snid 3998
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  e. 
_V
Assertion
Ref Expression
snid  |-  A  e. 
{ A }

Proof of Theorem snid
StepHypRef Expression
1 snid.1 . 2  |-  A  e. 
_V
2 snidb 3997 . 2  |-  ( A  e.  _V  <->  A  e.  { A } )
31, 2mpbi 212 1  |-  A  e. 
{ A }
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1889   _Vcvv 3047   {csn 3970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-v 3049  df-sn 3971
This theorem is referenced by:  ssnid  3999  rabsnt  4052  sneqr  4142  sseliALT  4539  elALT  4646  intid  4661  opthprc  4885  dmsnsnsn  5317  snsn0non  5544  fvrn0  5892  fsn  6066  fsn2  6067  fnsnb  6088  fmptsng  6090  fmptsnd  6091  fvsn  6102  fvsnun1  6104  ovima0  6453  brtpos0  6985  tfrlem11  7111  mapsn  7518  mapsncnv  7523  0elixp  7558  domunsncan  7677  enfixsn  7686  infeq5i  8146  tc2  8231  isfin4-3  8750  fin1a2lem12  8846  dcomex  8882  axdc3lem4  8888  zornn0g  8940  axpowndlem3  9029  canthp1lem2  9083  elreal2  9561  xrinfmss  11602  fseq1p1m1  11875  1exp  12308  wrdexb  12690  0bits  14425  lcmfunsnlem2  14625  0ram  14990  setsid  15176  imasvscafn  15455  imasvscaval  15456  xpsc0  15478  xpsc1  15479  gsumval2  16535  gsumz  16633  psgnsn  17173  psgnprfval2  17176  mat0dimscm  19506  mat0scmat  19575  mvmumamul1  19591  m1detdiag  19634  pmatcoe1fsupp  19737  d0mat2pmat  19774  pmatcollpw3fi1lem1  19822  pmatcollpw3fi1lem2  19823  chpmat0d  19870  dfac14  20645  filcon  20910  uffix  20948  cnextfvval  21092  cnextcn  21094  ust0  21246  bndth  21998  minveclem4a  22384  minveclem4aOLD  22396  dvef  22944  tdeglem2  23022  mdegcl  23030  aalioulem2  23301  cxplogb  23735  xrlimcnp  23906  axlowdimlem8  24991  axlowdimlem11  24994  vdgrf  25638  frgrancvvdeqlem7  25776  frgrancvvdeqlemA  25777  grposn  25955  rngosn  26144  hsn0elch  26913  rabsnel  28150  aciunf1lem  28276  esum2dlem  28925  signstfvn  29470  bnj145OLD  29547  bnj97  29689  bnj553  29721  bnj966  29767  bnj1442  29870  subfacp1lem2a  29915  subfacp1lem5  29919  cvmliftlem4  30023  ghomsn  30318  bj-0eltag  31584  poimirlem3  31955  poimirlem9  31961  poimirlem31  31983  poimirlem32  31984  prdsbnd  32137  heiborlem3  32157  grpokerinj  32195  0idl  32270  0rngo  32272  fvilbdRP  36294  frege54cor1c  36523  binomcxplemnotnn0  36716  snsslVD  37235  snssl  37236  unipwrVD  37238  unipwr  37239  sucidALTVD  37277  sucidALT  37278  sucidVD  37279  unisnALT  37333  mapsnd  37486  0cnf  37764  dvmptfprod  37830  qndenserrnbl  38174  nnfoctbdjlem  38303  isomenndlem  38361  hoidmvlelem2  38428  hoiqssbl  38457  funressnfv  38639  el1fzopredsuc  38732  1wlk1walk  39656  1wlk2v2elem1  39751  c0snmhm  40019  lincval0  40312  lcoel0  40325
  Copyright terms: Public domain W3C validator