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

Theorem snid 3670
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 3669 . 2  |-  ( A  e.  _V  <->  A  e.  { A } )
31, 2mpbi 201 1  |-  A  e. 
{ A }
Colors of variables: wff set class
Syntax hints:    e. wcel 1687   _Vcvv 2791   {csn 3643
This theorem is referenced by:  rabsnt  3707  sneqr  3783  elALT  4219  rext  4223  unipw  4225  intid  4232  snsn0non  4512  snnex  4525  reusv6OLD  4546  opthprc  4737  dmsnsnsn  5151  fvrn0  5513  fsn  5659  fsn2  5661  fnressn  5668  fressnfv  5670  fvsn  5676  fvsnun1  5678  brtpos0  6204  opabiota  6288  tfrlem11  6401  mapsn  6806  mapsncnv  6811  0elixp  6844  domunsncan  6959  ac6sfi  7098  iunfi  7141  elirrv  7308  infeq5i  7334  tc2  7424  dfac9  7759  kmlem2  7774  isfin4-3  7938  fin1a2lem10  8032  fin1a2lem12  8034  hsmexlem4  8052  dcomex  8070  axdc3lem4  8076  zornn0g  8129  iunfo  8158  axpowndlem3  8218  canthp1lem2  8272  elreal2  8751  xrinfmss  10624  fseq1p1m1  10853  1exp  11127  wrdexb  11445  fsumcom2  12233  0bits  12626  0ram  13063  setsid  13183  imasvscafn  13435  imasvscaval  13436  xpsc0  13458  xpsc1  13459  gsumz  14454  gsumval2  14456  islbs3  15904  lbsextlem4  15910  dishaus  17106  dis2ndc  17182  dislly  17219  dfac14  17308  txdis  17322  txdis1cn  17325  txkgen  17342  filcon  17574  isufil2  17599  uffix  17612  ufinffr  17620  alexsubALTlem4  17740  tmdgsum  17774  dscopn  18092  bndth  18452  minveclem4a  18790  ovolfiniun  18856  volfiniun  18900  i1fd  19032  dvef  19323  tdeglem2  19443  mdegcl  19451  aalioulem2  19709  xrlimcnp  20259  jensen  20279  grposn  20876  rngosn  21065  hsn0elch  21821  subfacp1lem2a  23117  subfacp1lem5  23121  cvmliftlem4  23225  cvmlift2lem1  23239  ghomsn  23401  wfrlem14  23672  wfrlem16  23674  funpartfv  23892  axlowdimlem8  23986  axlowdimlem11  23989  onint1  24297  limvinlv  24960  1ded  25139  comppfsc  25708  prdsbnd  25918  heiborlem3  25938  grpokerinj  25976  0idl  26051  0rngo  26053  mzpcompact2lem  26230  uvcff  26641  frlmlbs  26650  enfixsn  26658  islindf4  26709  funressnfv  27372  snsslVD  27874  snssl  27875  unipwrVD  27878  unipwr  27879  sucidALTVD  27916  sucidALT  27917  sucidVD  27918  unisnALT  27972  bnj145  28024  bnj97  28167  bnj553  28199  bnj966  28245  bnj1442  28348  bnj1498  28360  pclfinN  29358
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870  ax-ext 2267
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1531  df-nf 1534  df-sb 1633  df-clab 2273  df-cleq 2279  df-clel 2282  df-nfc 2411  df-v 2793  df-sn 3649
  Copyright terms: Public domain W3C validator