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

Theorem snid 3571
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 3570 . 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 2727   {csn 3544
This theorem is referenced by:  rabsnt  3608  sneqr  3680  elALT  4112  rext  4116  unipw  4118  intid  4125  snsn0non  4402  snnex  4415  reusv6OLD  4436  opthprc  4643  dmsnsnsn  5057  fvrn0  5403  fsn  5548  fsn2  5550  fnressn  5557  fressnfv  5559  fvsn  5565  fvsnun1  5567  brtpos0  6093  opabiota  6177  tfrlem11  6290  mapsn  6695  mapsncnv  6700  0elixp  6733  domunsncan  6847  ac6sfi  6986  iunfi  7029  elirrv  7195  infeq5i  7221  tc2  7311  dfac9  7646  kmlem2  7661  isfin4-3  7825  fin1a2lem10  7919  fin1a2lem12  7921  hsmexlem4  7939  dcomex  7957  axdc3lem4  7963  zornn0g  8016  iunfo  8045  axpowndlem3  8101  canthp1lem2  8155  elreal2  8634  xrinfmss  10506  fseq1p1m1  10735  1exp  11009  wrdexb  11326  fsumcom2  12114  0bits  12504  0ram  12941  setsid  13061  imasvscafn  13313  imasvscaval  13314  xpsc0  13336  xpsc1  13337  gsumz  14293  gsumval2  14295  islbs3  15742  lbsextlem4  15746  dishaus  16942  dis2ndc  17018  dislly  17055  dfac14  17144  txdis  17158  txdis1cn  17161  txkgen  17178  filcon  17410  isufil2  17435  uffix  17448  ufinffr  17456  alexsubALTlem4  17576  tmdgsum  17610  dscopn  17928  bndth  18288  minveclem4a  18626  ovolfiniun  18692  volfiniun  18736  i1fd  18868  dvef  19159  tdeglem2  19279  mdegcl  19287  aalioulem2  19545  xrlimcnp  20095  jensen  20115  grposn  20712  rngosn  20901  hsn0elch  21657  subfacp1lem2a  22882  subfacp1lem5  22886  cvmliftlem4  22990  cvmlift2lem1  23004  ghomsn  23166  wfrlem14  23437  wfrlem16  23439  funpartfv  23657  axlowdimlem8  23751  axlowdimlem11  23754  onint1  24062  limvinlv  24725  1ded  24904  comppfsc  25473  prdsbnd  25683  heiborlem3  25703  grpokerinj  25741  0idl  25816  0rngo  25818  mzpcompact2lem  25995  uvcff  26406  frlmlbs  26415  enfixsn  26423  islindf4  26474  snsslVD  27294  snssl  27295  unipwrVD  27298  unipwr  27299  sucidALTVD  27336  sucidALT  27337  sucidVD  27338  unisnALT  27392  bnj145  27444  bnj97  27587  bnj553  27619  bnj966  27665  bnj1442  27768  bnj1498  27780  pclfinN  28778
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-sn 3550
  Copyright terms: Public domain W3C validator