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

Theorem snid 3608
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 3607 . 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 2740   {csn 3581
This theorem is referenced by:  rabsnt  3645  sneqr  3721  elALT  4156  rext  4160  unipw  4162  intid  4169  snsn0non  4448  snnex  4461  reusv6OLD  4482  opthprc  4689  dmsnsnsn  5103  fvrn0  5449  fsn  5595  fsn2  5597  fnressn  5604  fressnfv  5606  fvsn  5612  fvsnun1  5614  brtpos0  6140  opabiota  6224  tfrlem11  6337  mapsn  6742  mapsncnv  6747  0elixp  6780  domunsncan  6895  ac6sfi  7034  iunfi  7077  elirrv  7244  infeq5i  7270  tc2  7360  dfac9  7695  kmlem2  7710  isfin4-3  7874  fin1a2lem10  7968  fin1a2lem12  7970  hsmexlem4  7988  dcomex  8006  axdc3lem4  8012  zornn0g  8065  iunfo  8094  axpowndlem3  8154  canthp1lem2  8208  elreal2  8687  xrinfmss  10559  fseq1p1m1  10788  1exp  11062  wrdexb  11379  fsumcom2  12167  0bits  12557  0ram  12994  setsid  13114  imasvscafn  13366  imasvscaval  13367  xpsc0  13389  xpsc1  13390  gsumz  14385  gsumval2  14387  islbs3  15835  lbsextlem4  15841  dishaus  17037  dis2ndc  17113  dislly  17150  dfac14  17239  txdis  17253  txdis1cn  17256  txkgen  17273  filcon  17505  isufil2  17530  uffix  17543  ufinffr  17551  alexsubALTlem4  17671  tmdgsum  17705  dscopn  18023  bndth  18383  minveclem4a  18721  ovolfiniun  18787  volfiniun  18831  i1fd  18963  dvef  19254  tdeglem2  19374  mdegcl  19382  aalioulem2  19640  xrlimcnp  20190  jensen  20210  grposn  20807  rngosn  20996  hsn0elch  21752  subfacp1lem2a  23048  subfacp1lem5  23052  cvmliftlem4  23156  cvmlift2lem1  23170  ghomsn  23332  wfrlem14  23603  wfrlem16  23605  funpartfv  23823  axlowdimlem8  23917  axlowdimlem11  23920  onint1  24228  limvinlv  24891  1ded  25070  comppfsc  25639  prdsbnd  25849  heiborlem3  25869  grpokerinj  25907  0idl  25982  0rngo  25984  mzpcompact2lem  26161  uvcff  26572  frlmlbs  26581  enfixsn  26589  islindf4  26640  snsslVD  27617  snssl  27618  unipwrVD  27621  unipwr  27622  sucidALTVD  27659  sucidALT  27660  sucidVD  27661  unisnALT  27715  bnj145  27767  bnj97  27910  bnj553  27942  bnj966  27988  bnj1442  28091  bnj1498  28103  pclfinN  29219
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 2237
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-sn 3587
  Copyright terms: Public domain W3C validator