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

Theorem snssi 4014
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 4004 . 2  |-  ( A  e.  B  ->  ( A  e.  B  <->  { A }  C_  B ) )
21ibi 241 1  |-  ( A  e.  B  ->  { A }  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1761    C_ wss 3325   {csn 3874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-v 2972  df-in 3332  df-ss 3339  df-sn 3875
This theorem is referenced by:  difsnid  4016  pwpw0  4018  sssn  4028  ssunsn2  4029  tpssi  4036  pwsnALT  4083  snelpwi  4534  intid  4547  xpsspw  4949  xpsspwOLD  4950  djussxp  4981  xpimasnOLD  5281  fconst6g  5596  dffv2  5761  fvimacnvi  5814  fvimacnvALT  5819  fsn2  5880  fsnunf  5913  suceloni  6423  curry1  6663  curry2  6666  ressuppss  6707  ressuppssdif  6709  mapsn  7250  ralxpmap  7258  fodomr  7458  sucdom2  7503  en1eqsn  7538  enp1ilem  7542  findcard2  7548  findcard2s  7549  marypha1lem  7679  marypha2lem1  7681  epfrs  7947  dfac5lem4  8292  kmlem11  8325  ackbij1lem2  8386  fin23lem26  8490  isfin1-3  8551  hsmexlem4  8594  axdc3lem4  8618  axresscn  9311  nn0ssre  10579  xrsupss  11267  supxrmnf  11276  1fv  11528  1exp  11889  hashxrcl  12123  hashdifsn  12165  brfi1indlem  12214  snopiswrd  12239  repsdf2  12412  fsum00  13257  incexc  13296  xpnnenOLD  13488  2ebits  13639  bitsinvp1  13641  4sqlem19  14020  ramxrcl  14074  strlemor1  14261  mrcsncl  14546  acsfn1  14595  homaf  14894  dmcoass  14930  lubel  15288  gsumws1  15510  cycsubg2  15711  cntzsnval  15835  0frgp  16269  dpjidcl  16547  dpjidclOLD  16554  ablfac1eu  16564  lspsncl  17036  lspsnss  17049  lspsnid  17052  lpival  17305  lpiss  17310  lidldvgen  17315  znlidl  17923  znlidlOLD  17927  frgpcyg  17965  frlmlbs  18184  smadiadetglem2  18437  isneip  18668  neips  18676  opnneip  18682  maxlp  18710  restsn2  18734  leordtval2  18775  ist1-3  18912  ordtt1  18942  2ndcdisj2  19020  uffix  19453  neiflim  19506  ptcmplem5  19587  cnextfres  19599  haustsms2  19666  ust0  19753  ustuqtop5  19779  dscopn  20125  icccmplem1  20358  bndth  20489  ovolsn  20937  icombl1  21003  plyun0  21624  coeeulem  21651  coeeu  21652  vieta1lem2  21736  aalioulem2  21758  taylfval  21783  perfectlem2  22528  axlowdimlem7  23129  axlowdimlem10  23132  konigsberg  23543  hsn0elch  24586  chsupsn  24751  chsup0  24886  h1deoi  24887  h1dei  24888  h1did  24889  h1de2ctlem  24893  h1de2ci  24894  spansni  24895  spansnch  24898  elspansncl  24903  spansnpji  24916  spanunsni  24917  spanpr  24918  h1datomi  24919  spansnji  24984  h1da  25688  atom1d  25692  superpos  25693  resf1o  25965  esumnul  26438  esumcst  26450  hashf2  26469  measvuni  26564  cntnevol  26578  eulerpartlemt  26684  eulerpartlemmf  26688  eulerpartlemgh  26691  ballotlemfp1  26804  dfon2lem3  27527  altxpsspw  27937  mblfinlem2  28354  dvasin  28405  fdc  28566  prnc  28792  isfldidl  28793  ispridlc  28795  mapfzcons  28977  mzpcompact2lem  29013  diophrw  29022  stoweidlem44  29764  dmressnsn  29953  fnbrafvb  29985  afvres  30003  modfsummods  30169  mapsnop  30659  mat1dimelbas  30750  mat1dimmul  30755  lincext2  30830  snlindsntorlem  30845  snelpwrVD  31401  bj-snglss  32193  islshpsm  32347  snatpsubN  33116  polatN  33297  atpsubclN  33311  pclfinclN  33316
  Copyright terms: Public domain W3C validator