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

Theorem snid 3893
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 3892 . 2  |-  ( A  e.  _V  <->  A  e.  { A } )
31, 2mpbi 208 1  |-  A  e. 
{ A }
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1755   _Vcvv 2962   {csn 3865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-sn 3866
This theorem is referenced by:  ssnid  3894  rabsnt  3940  sneqr  4028  sseliALT  4411  reusv6OLD  4491  elALT  4523  intid  4538  snsn0non  4824  opthprc  4873  dmsnsnsn  5305  fvrn0  5700  fsn  5868  fsn2  5870  fnsnb  5885  fmptsng  5887  fvsn  5898  fvsnun1  5900  ovima0  6231  brtpos0  6741  tfrlem11  6833  mapsn  7242  mapsncnv  7247  0elixp  7282  domunsncan  7399  enfixsn  7408  findcard2d  7542  infeq5i  7830  tc2  7950  isfin4-3  8472  fin1a2lem12  8568  dcomex  8604  axdc3lem4  8610  zornn0g  8662  axpowndlem3  8752  axpowndlem3OLD  8753  canthp1lem2  8808  elreal2  9287  xrinfmss  11260  fseq1p1m1  11518  1exp  11877  wrdexb  12229  0bits  13618  0ram  14064  setsid  14198  imasvscafn  14458  imasvscaval  14459  xpsc0  14481  xpsc1  14482  gsumz  15491  gsumval2  15493  psgnprfval2  16007  mvmumamul1  18207  maducoeval2  18288  dfac14  19033  filcon  19298  uffix  19336  cnextfvval  19479  cnextcn  19481  ust0  19636  bndth  20372  minveclem4a  20759  dvef  21294  tdeglem2  21415  mdegcl  21425  aalioulem2  21684  xrlimcnp  22247  axlowdimlem8  23018  axlowdimlem11  23021  vdgrf  23391  grposn  23525  rngosn  23714  hsn0elch  24474  rabsnel  25711  signstfvn  26818  subfacp1lem2a  26916  subfacp1lem5  26920  cvmliftlem4  27025  ghomsn  27154  prdsbnd  28536  heiborlem3  28556  grpokerinj  28594  0idl  28669  0rngo  28671  funressnfv  29880  frgrancvvdeqlem7  30475  frgrancvvdeqlemA  30476  fmptsnd  30567  psgnsn  30603  mat0dimscm  30654  m1detdiag  30664  lincval0  30679  lcoel0  30692  snsslVD  31288  snssl  31289  unipwrVD  31291  unipwr  31292  sucidALTVD  31329  sucidALT  31330  sucidVD  31331  unisnALT  31385  bnj145OLD  31441  bnj97  31582  bnj553  31614  bnj966  31660  bnj1442  31763  bj-0eltag  32075
  Copyright terms: Public domain W3C validator