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

Theorem syl6eqss 3358
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 3342 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    C_ wss 3280
This theorem is referenced by:  syl6eqssr  3359  dmxpss  5259  dmsnopss  5301  iotassuni  5393  fvmptss  5772  fvmptss2  5783  fimacnv  5821  funressn  5878  frxp  6415  riotassuni  6547  oawordeulem  6756  omwordri  6774  oewordri  6794  map0e  7010  fodomr  7217  fipwuni  7389  fipwss  7392  ordtypelem6  7448  inf3lemd  7538  cantnfle  7582  cantnflem2  7602  ackbij1lem15  8070  ackbij2lem3  8077  cfub  8085  cflecard  8089  cfle  8090  fin23lem13  8168  fin23lem29  8177  compsscnvlem  8206  itunitc1  8256  fpwwe2lem12  8472  grur1a  8650  uzssz  10461  limsupgle  12226  isercolllem2  12414  isercoll  12416  fsumss  12474  sadcaddlem  12924  sadadd2lem  12926  sadadd3  12928  sadcl  12929  sadaddlem  12933  sadasslem  12937  sadeq  12939  smupvallem  12950  smucl  12951  prmreclem4  13242  prmreclem5  13243  1arith  13250  vdwmc2  13302  vdwlem13  13316  ramz2  13347  strfvss  13442  ressbasss  13476  prdsless  13640  sectss  13933  invss  13941  fullfunc  14058  fthfunc  14059  catccatid  14212  resscatc  14215  catcisolem  14216  catciso  14217  yoniso  14337  cntzrcl  15081  cntzssv  15082  ablfaclem3  15600  lmhmlsp  16080  resspsrbas  16433  resspsrvsca  16436  subrgpsr  16437  mplsubglem  16453  ressmplbas  16474  subrgmpl  16478  ressply1bas  16578  cssss  16867  basdif0  16973  ntrss2  17076  ordtbas2  17209  ordtbas  17210  cncls  17292  cmpfi  17425  kgentopon  17523  ptpjpre1  17556  xkoccn  17604  prdstopn  17613  uzfbas  17883  utoptop  18217  utopbas  18218  setsmstopn  18461  restmetu  18570  tngtopn  18644  iccntr  18805  metdstri  18834  pi1xfrcnvlem  19034  cphsubrglem  19093  tchcph  19147  ovolshftlem1  19358  ovolshft  19360  ovolscalem1  19362  ovolscalem2  19363  ovolsca  19364  uniioombllem2  19428  uniioombllem3a  19429  uniioombllem3  19430  uniioombllem4  19431  uniioombllem6  19433  itgioo  19660  limcnlp  19718  dvbsss  19742  dvcnvrelem1  19854  dvfsumle  19858  dvfsumabs  19860  mpfrcl  19892  pserdv  20298  rlimcnp2  20758  fsumharmonic  20803  chpval2  20955  nbgrassvt  21398  subgornss  21847  ocsh  22738  shsss  22768  speccl  23355  elnlfn  23384  pj3i  23664  sumdmdlem2  23875  ssnnssfz  24101  gsumpropd2lem  24173  inftmrel  24203  metidss  24239  dya2iocuni  24586  kur14lem1  24845  cvmliftmolem2  24922  cvmliftlem15  24938  trpredlem1  25444  wfrlem15  25484  mblfinlem  26143  comppfsc  26277  sdclem2  26336  sstotbnd2  26373  isbnd3  26383  diophin  26721  frlmplusgval  27097  frlmvscafval  27098  itgocn  27237  en2other2  27250  stoweidlem34  27650  stoweidlem59  27675  swrdltnd  28000  bnj1143  28867  bnj1262  28888  bnj517  28962  lkrlss  29578  pmapssat  30241  diass  31525  diaintclN  31541  dia2dimlem13  31559  dibintclN  31650  lcfrlem25  32050  lcdvbasess  32077  mapdin  32145
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator