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

Theorem snid 3641
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 3640 . 2  |-  ( A  e.  _V  <->  A  e.  { A } )
31, 2mpbi 201 1  |-  A  e. 
{ A }
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   _Vcvv 2763   {csn 3614
This theorem is referenced by:  rabsnt  3678  sneqr  3754  elALT  4190  rext  4194  unipw  4196  intid  4203  snsn0non  4483  snnex  4496  reusv6OLD  4517  opthprc  4724  dmsnsnsn  5138  fvrn0  5484  fsn  5630  fsn2  5632  fnressn  5639  fressnfv  5641  fvsn  5647  fvsnun1  5649  brtpos0  6175  opabiota  6259  tfrlem11  6372  mapsn  6777  mapsncnv  6782  0elixp  6815  domunsncan  6930  ac6sfi  7069  iunfi  7112  elirrv  7279  infeq5i  7305  tc2  7395  dfac9  7730  kmlem2  7745  isfin4-3  7909  fin1a2lem10  8003  fin1a2lem12  8005  hsmexlem4  8023  dcomex  8041  axdc3lem4  8047  zornn0g  8100  iunfo  8129  axpowndlem3  8189  canthp1lem2  8243  elreal2  8722  xrinfmss  10594  fseq1p1m1  10823  1exp  11097  wrdexb  11414  fsumcom2  12202  0bits  12592  0ram  13029  setsid  13149  imasvscafn  13401  imasvscaval  13402  xpsc0  13424  xpsc1  13425  gsumz  14420  gsumval2  14422  islbs3  15870  lbsextlem4  15876  dishaus  17072  dis2ndc  17148  dislly  17185  dfac14  17274  txdis  17288  txdis1cn  17291  txkgen  17308  filcon  17540  isufil2  17565  uffix  17578  ufinffr  17586  alexsubALTlem4  17706  tmdgsum  17740  dscopn  18058  bndth  18418  minveclem4a  18756  ovolfiniun  18822  volfiniun  18866  i1fd  18998  dvef  19289  tdeglem2  19409  mdegcl  19417  aalioulem2  19675  xrlimcnp  20225  jensen  20245  grposn  20842  rngosn  21031  hsn0elch  21787  subfacp1lem2a  23083  subfacp1lem5  23087  cvmliftlem4  23191  cvmlift2lem1  23205  ghomsn  23367  wfrlem14  23638  wfrlem16  23640  funpartfv  23858  axlowdimlem8  23952  axlowdimlem11  23955  onint1  24263  limvinlv  24926  1ded  25105  comppfsc  25674  prdsbnd  25884  heiborlem3  25904  grpokerinj  25942  0idl  26017  0rngo  26019  mzpcompact2lem  26196  uvcff  26607  frlmlbs  26616  enfixsn  26624  islindf4  26675  snsslVD  27654  snssl  27655  unipwrVD  27658  unipwr  27659  sucidALTVD  27696  sucidALT  27697  sucidVD  27698  unisnALT  27752  bnj145  27804  bnj97  27947  bnj553  27979  bnj966  28025  bnj1442  28128  bnj1498  28140  pclfinN  29256
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-sn 3620
  Copyright terms: Public domain W3C validator