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

Theorem snid 3833
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 3832 . 2  |-  ( A  e.  _V  <->  A  e.  { A } )
31, 2mpbi 200 1  |-  A  e. 
{ A }
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   _Vcvv 2948   {csn 3806
This theorem is referenced by:  exsnrex  3840  rabsnt  3873  sneqr  3958  elALT  4399  rext  4404  unipw  4406  intid  4413  snsn0non  4691  snnex  4704  reusv6OLD  4725  opthprc  4916  dmsnsnsn  5339  fvrn0  5744  fsn  5897  fsn2  5899  fnressn  5909  fressnfv  5911  fvsn  5917  fvsnun1  5919  brtpos0  6477  opabiota  6529  tfrlem11  6640  mapsn  7046  mapsncnv  7051  0elixp  7084  domunsncan  7199  ac6sfi  7342  iunfi  7385  elirrv  7554  infeq5i  7580  tc2  7670  kmlem2  8020  isfin4-3  8184  fin1a2lem10  8278  fin1a2lem12  8280  hsmexlem4  8298  dcomex  8316  axdc3lem4  8322  zornn0g  8374  iunfo  8403  axpowndlem3  8463  canthp1lem2  8517  elreal2  8996  xrinfmss  10877  fseq1p1m1  11110  1exp  11397  wrdexb  11751  fsumcom2  12546  0bits  12939  0ram  13376  setsid  13496  imasvscafn  13750  imasvscaval  13751  xpsc0  13773  xpsc1  13774  gsumz  14769  gsumval2  14771  lbsextlem4  16221  dishaus  17434  dis2ndc  17511  dislly  17548  dfac14  17638  txdis  17652  txdis1cn  17655  txkgen  17672  filcon  17903  isufil2  17928  uffix  17941  alexsubALTlem4  18069  cnextfvval  18084  cnextcn  18086  tmdgsum  18113  ust0  18237  dscopn  18609  bndth  18971  minveclem4a  19319  ovolfiniun  19385  volfiniun  19429  dvef  19852  tdeglem2  19972  mdegcl  19980  aalioulem2  20238  xrlimcnp  20795  jensen  20815  cusgrares  21469  uvtx01vtx  21489  vdgrf  21657  grposn  21791  rngosn  21980  hsn0elch  22738  subfacp1lem2a  24854  subfacp1lem5  24858  cvmliftlem4  24963  cvmlift2lem1  24977  ghomsn  25087  fprodcom2  25297  wfrlem14  25524  wfrlem16  25526  funpartlem  25737  axlowdimlem8  25836  axlowdimlem11  25839  mbfresfi  26199  comppfsc  26324  prdsbnd  26439  heiborlem3  26459  grpokerinj  26497  0idl  26572  0rngo  26574  mzpcompact2lem  26745  frlmlbs  27164  enfixsn  27172  funressnfv  27906  frgrancvvdeqlem3  28279  frgrancvvdeqlem4  28280  frgrancvvdeqlem7  28283  frgrancvvdeqlemA  28284  frgrawopreg1  28297  frgrawopreg2  28298  snsslVD  28795  snssl  28796  unipwrVD  28798  unipwr  28799  sucidALTVD  28836  sucidALT  28837  sucidVD  28838  unisnALT  28892  bnj145  28948  bnj97  29091  bnj553  29123  bnj966  29169  bnj1442  29272  bnj1498  29284  pclfinN  30536
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-sn 3812
  Copyright terms: Public domain W3C validator