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

Theorem syl6eqss 3504
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 3488 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    C_ wss 3426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3433  df-ss 3440
This theorem is referenced by:  syl6eqssr  3505  dmxpss  5367  dmsnopss  5409  iotassuni  5495  fvmptss  5881  fvmptss2  5892  fimacnv  5934  funressn  5994  riotassuniOLD  6188  frxp  6782  suppssdm  6803  suppun  6809  suppss  6819  suppssov1  6821  suppss2  6823  suppssfv  6825  oawordeulem  7093  omwordri  7111  oewordri  7131  map0e  7350  fodomr  7562  fipwuni  7777  fipwss  7780  ordtypelem6  7838  inf3lemd  7934  cantnfle  7980  cantnflem2  7999  cantnfleOLD  8010  en2other2  8277  ackbij1lem15  8504  ackbij2lem3  8511  cfub  8519  cflecard  8523  cfle  8524  fin23lem13  8602  fin23lem29  8611  compsscnvlem  8640  itunitc1  8690  fpwwe2lem12  8909  grur1a  9087  uzssz  10981  swrdlend  12427  repswswrd  12524  limsupgle  13057  isercolllem2  13245  isercoll  13247  fsumss  13304  sadcaddlem  13755  sadadd2lem  13757  sadadd3  13759  sadcl  13760  sadaddlem  13764  sadasslem  13768  sadeq  13770  smupvallem  13781  smucl  13782  prmreclem4  14082  prmreclem5  14083  1arith  14090  vdwmc2  14142  vdwlem13  14156  ramz2  14187  strfvss  14294  ressbasss  14332  prdsless  14503  sectss  14793  invss  14801  fullfunc  14918  fthfunc  14919  catccatid  15072  resscatc  15075  catcisolem  15076  catciso  15077  yoniso  15197  gsumpropd2lem  15607  cntzrcl  15947  cntzssv  15948  ablfaclem3  16693  lmhmlsp  17236  resspsrbas  17594  resspsrvsca  17597  subrgpsr  17598  mplsubglem  17617  mplsubglemOLD  17619  ressmplbas  17642  subrgmpl  17646  mpfrcl  17711  ressply1bas  17790  ply1coeOLD  17856  evpmss  18125  cssss  18219  frlmplusgval  18300  frlmvscafval  18302  uvcresum  18327  basdif0  18674  ntrss2  18777  ordtbas2  18911  ordtbas  18912  cncls  18994  cmpfi  19127  kgentopon  19227  ptpjpre1  19260  xkoccn  19308  prdstopn  19317  uzfbas  19587  utoptop  19925  utopbas  19926  setsmstopn  20169  restmetu  20278  tngtopn  20352  iccntr  20514  metdstri  20543  pi1xfrcnvlem  20744  cphsubrglem  20812  tchcph  20868  rrxnm  21011  ovolshftlem1  21108  ovolshft  21110  ovolscalem1  21112  ovolscalem2  21113  ovolsca  21114  uniioombllem2  21179  uniioombllem3a  21180  uniioombllem3  21181  uniioombllem4  21182  uniioombllem6  21184  itgioo  21409  limcnlp  21469  dvbsss  21493  dvcnvrelem1  21605  dvfsumle  21609  dvfsumabs  21611  pserdv  22010  rlimcnp2  22476  fsumharmonic  22521  chpval2  22673  tglnssp  23105  perpln1  23229  perpln2  23230  nbgrassvt  23479  subgornss  23928  ocsh  24821  shsss  24851  speccl  25438  elnlfn  25467  pj3i  25747  sumdmdlem2  25958  ffsrn  26163  ssnnssfz  26210  inftmrel  26331  metidss  26452  fsumcvg4  26514  dya2iocuni  26832  kur14lem1  27228  cvmliftmolem2  27305  cvmliftlem15  27321  trpredlem1  27825  wfrlem15  27872  mblfinlem2  28567  comppfsc  28717  sdclem2  28776  sstotbnd2  28811  isbnd3  28821  diophin  29249  itgocn  29659  stoweidlem34  29967  stoweidlem59  29992  clwwlksswrd  30578  ssnn0ssfz  30879  fsuppmapnn0fiublem  30936  fsuppmapnn0fiub  30937  cpmatsubgpmat  31183  bnj1143  32084  bnj1262  32104  bnj517  32178  lkrlss  33046  pmapssat  33709  diass  34993  diaintclN  35009  dia2dimlem13  35027  dibintclN  35118  lcfrlem25  35518  lcdvbasess  35545  mapdin  35613
  Copyright terms: Public domain W3C validator