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

Theorem syl6eqss 3511
Description: A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
syl6eqss.1  |-  ( ph  ->  A  =  B )
syl6eqss.2  |-  B  C_  C
Assertion
Ref Expression
syl6eqss  |-  ( ph  ->  A  C_  C )

Proof of Theorem syl6eqss
StepHypRef Expression
1 syl6eqss.1 . 2  |-  ( ph  ->  A  =  B )
2 syl6eqss.2 . . 3  |-  B  C_  C
32a1i 11 . 2  |-  ( ph  ->  B  C_  C )
41, 3eqsstrd 3495 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    C_ wss 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-in 3440  df-ss 3447
This theorem is referenced by:  syl6eqssr  3512  dmxpss  5279  dmsnopss  5319  iotassuni  5572  fvmptss  5965  fvmptss2  5976  fimacnv  6018  funressn  6083  riotassuni  6294  frxp  6908  suppssdm  6929  suppun  6937  suppss  6947  suppssov1  6949  suppss2  6951  suppssfv  6953  wfrlem15  7049  oawordeulem  7254  omwordri  7272  oewordri  7292  fodomr  7720  fipwuni  7937  fipwss  7940  ordtypelem6  8029  inf3lemd  8123  cantnfle  8166  cantnflem2  8185  en2other2  8430  ackbij1lem15  8653  ackbij2lem3  8660  cfub  8668  cflecard  8672  cfle  8673  fin23lem13  8751  fin23lem29  8760  compsscnvlem  8789  itunitc1  8839  fpwwe2lem12  9055  grur1a  9233  uzssz  11167  fsuppmapnn0fiublem  12188  fsuppmapnn0fiub  12189  swrdlend  12761  repswswrd  12861  xptrrel  13012  relexpnndm  13072  limsupgle  13502  isercolllem2  13696  isercoll  13698  fsumss  13758  sadcaddlem  14394  sadadd2lem  14396  sadadd3  14398  sadcl  14399  sadaddlem  14403  sadasslem  14407  sadeq  14409  smupvallem  14420  smucl  14421  prmreclem4  14815  prmreclem5  14816  1arith  14823  vdwmc2  14881  vdwlem13  14895  ramz2  14934  strfvss  15091  ressbasss  15133  prdsless  15313  sectss  15601  invss  15610  fullfunc  15755  fthfunc  15756  catccatid  15941  resscatc  15944  catcisolem  15945  catciso  15946  yoniso  16114  gsumpropd2lem  16460  cntzrcl  16925  cntzssv  16926  gsumzmhm  17498  ablfaclem3  17648  lmhmlsp  18200  resspsrbas  18567  resspsrvsca  18570  subrgpsr  18571  mplsubglem  18586  ressmplbas  18608  subrgmpl  18612  mpfrcl  18669  ressply1bas  18750  ply1coeOLD  18818  evpmss  19078  cssss  19172  frlmplusgval  19250  frlmvscafval  19252  uvcresum  19275  scmatlss  19474  cpmatsubgpmat  19668  basdif0  19892  ntrss2  19996  ordtbas2  20131  ordtbas  20132  cncls  20214  cmpfi  20347  comppfsc  20471  kgentopon  20477  ptpjpre1  20510  xkoccn  20558  prdstopn  20567  uzfbas  20837  utoptop  21173  utopbas  21174  setsmstopn  21417  restmetu  21509  tngtopn  21582  iccntr  21743  metdstri  21772  pi1xfrcnvlem  21973  cphsubrglem  22041  tchcph  22097  rrxnm  22236  ovolshftlem1  22336  ovolshft  22338  ovolscalem1  22340  ovolscalem2  22341  ovolsca  22342  uniioombllem2  22414  uniioombllem2OLD  22415  uniioombllem3a  22416  uniioombllem3  22417  uniioombllem4  22418  uniioombllem6  22420  itgioo  22647  limcnlp  22707  dvbsss  22731  dvcnvrelem1  22843  dvfsumle  22847  dvfsumabs  22849  pserdv  23246  rlimcnp2  23754  fsumharmonic  23799  chpval2  24006  tglnssp  24454  perpln1  24609  perpln2  24610  nbgrassvt  25003  clwwlksswrd  25347  subgornss  25876  ocsh  26768  shsss  26798  speccl  27384  elnlfn  27413  pj3i  27693  sumdmdlem2  27904  fcoinver  28050  ffsrn  28154  ssnnssfz  28200  inftmrel  28332  smatrcl  28458  metidss  28530  fsumcvg4  28592  dya2iocuni  28941  carsgcl  28962  bnj1143  29387  bnj1262  29407  bnj517  29481  kur14lem1  29714  cvmliftmolem2  29790  cvmliftlem15  29806  mrsubrn  29936  msubrn  29952  trpredlem1  30252  poimirlem30  31674  mblfinlem2  31682  sdclem2  31775  sstotbnd2  31810  isbnd3  31820  lkrlss  32370  pmapssat  33033  diass  34319  diaintclN  34335  dia2dimlem13  34353  dibintclN  34444  lcfrlem25  34844  lcdvbasess  34871  mapdin  34939  diophin  35324  itgocn  35733  relexp0a  35951  frege131d  35999  ibliooicc  37421  stoweidlem34  37468  stoweidlem59  37493  etransclem24  37694  caratheodory  37862  rnghmresfn  38736  rnghmsscmap2  38746  rnghmsscmap  38747  rngchomrnghmresALTV  38769  funcrngcsetc  38771  rhmresfn  38782  dfringc2  38791  rhmsscmap2  38792  rhmsscmap  38793  rhmsscrnghm  38799  funcringcsetc  38808  funcringcsetcALTV2lem9  38817  rngcrescrhm  38858  rhmsubclem1  38859  rhmsubclem4  38862  rngcrescrhmALTV  38877  rhmsubcALTVlem1  38878  ssnn0ssfz  38903
  Copyright terms: Public domain W3C validator