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

Theorem snssi 3857
Description: The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.)
Assertion
Ref Expression
snssi  |-  ( A  e.  B  ->  { A }  C_  B )

Proof of Theorem snssi
StepHypRef Expression
1 snssg 3847 . 2  |-  ( A  e.  B  ->  ( A  e.  B  <->  { A }  C_  B ) )
21ibi 232 1  |-  ( A  e.  B  ->  { A }  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1715    C_ wss 3238   {csn 3729
This theorem is referenced by:  difsnid  3859  pwpw0  3861  sssn  3872  ssunsn2  3873  pwsnALT  3924  snelpwi  4322  intid  4334  suceloni  4707  xpsspw  4900  xpsspwOLD  4901  djussxp  4932  fconst6g  5536  dffv2  5699  fvimacnvi  5746  fvimacnvALT  5751  fsn2  5809  fsnunf  5831  curry1  6338  curry2  6341  mapsn  6952  fodomr  7155  sucdom2  7200  en1eqsn  7235  enp1ilem  7239  findcard2  7245  findcard2s  7246  marypha1lem  7333  marypha2lem1  7335  epfrs  7560  dfac5lem4  7900  kmlem11  7933  ackbij1lem2  7994  fin23lem26  8098  isfin1-3  8159  hsmexlem4  8202  axdc3lem4  8226  axresscn  8917  nn0ssre  10118  xrsupss  10780  supxrmnf  10789  1fv  11010  1exp  11296  hashxrcl  11527  hashdifsn  11566  brfi1indlem  11601  s1cl  11642  fsum00  12464  incexclem  12503  incexc  12504  xpnnenOLD  12696  2ebits  12846  bitsinvp1  12848  4sqlem19  13218  ramxrcl  13272  strlemor1  13443  mrcsncl  13724  acsfn1  13773  homaf  14072  dmcoass  14108  lubel  14436  gsumws1  14672  cycsubg2  14864  cntzsnval  15010  0frgp  15298  dpjidcl  15503  ablfac1eu  15518  lspsncl  15944  lspsnss  15957  lspsnid  15960  lpival  16207  lpiss  16212  lidldvgen  16217  znlidl  16704  frgpcyg  16744  isneip  17059  neips  17067  opnneip  17073  maxlp  17095  restsn2  17119  leordtval2  17159  ist1-3  17294  ordtt1  17324  2ndcdisj2  17400  uffix  17829  neiflim  17882  ptcmplem5  17963  haustsms2  18032  dscopn  18309  icccmplem1  18541  bndth  18671  ovolsn  19069  icombl1  19135  plyun0  19794  coeeulem  19821  coeeu  19822  vieta1lem2  19906  aalioulem2  19928  taylfval  19953  perfectlem2  20692  konigsberg  21220  hsn0elch  22261  chsupsn  22426  chsup0  22561  h1deoi  22562  h1dei  22563  h1did  22564  h1de2ctlem  22568  h1de2ci  22569  spansni  22570  spansnch  22573  elspansncl  22578  spansnpji  22591  spanunsni  22592  spanpr  22593  h1datomi  22594  spansnji  22659  h1da  23363  atom1d  23367  superpos  23368  ust0  23843  ustuqtop5  23869  esumnul  24029  esumcst  24041  hashf2  24060  measvuni  24152  cntnevol  24166  dfon2lem3  24967  altxpsspw  25338  axlowdimlem7  25403  axlowdimlem10  25406  dvreasin  25783  fdc  26047  prnc  26283  isfldidl  26284  ispridlc  26286  ralxpmap  26352  mapfzcons  26384  mzpcompact2lem  26420  diophrw  26429  frlmlbs  26840  stoweidlem44  27384  dmressnsn  27576  funcoressn  27583  funressnfv  27584  fnbrafvb  27610  afvres  27628  constr2trl  27745  snelpwrVD  28358  islshpsm  29229  snatpsubN  29998  polatN  30179  atpsubclN  30193  pclfinclN  30198
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-v 2875  df-in 3245  df-ss 3252  df-sn 3735
  Copyright terms: Public domain W3C validator