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

Theorem syl6eqss 3341
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 3325 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    C_ wss 3263
This theorem is referenced by:  syl6eqssr  3342  dmxpss  5240  dmsnopss  5282  iotassuni  5374  fvmptss  5752  fvmptss2  5763  fimacnv  5801  funressn  5858  frxp  6392  riotassuni  6524  oawordeulem  6733  omwordri  6751  oewordri  6771  map0e  6987  fodomr  7194  fipwuni  7366  fipwss  7369  ordtypelem6  7425  inf3lemd  7515  cantnfle  7559  cantnflem2  7579  ackbij1lem15  8047  ackbij2lem3  8054  cfub  8062  cflecard  8066  cfle  8067  fin23lem13  8145  fin23lem29  8154  compsscnvlem  8183  itunitc1  8233  fpwwe2lem12  8449  grur1a  8627  uzssz  10437  limsupgle  12198  isercolllem2  12386  isercoll  12388  fsumss  12446  sadcaddlem  12896  sadadd2lem  12898  sadadd3  12900  sadcl  12901  sadaddlem  12905  sadasslem  12909  sadeq  12911  smupvallem  12922  smucl  12923  prmreclem4  13214  prmreclem5  13215  1arith  13222  vdwmc2  13274  vdwlem13  13288  ramz2  13319  strfvss  13414  ressbasss  13448  prdsless  13612  sectss  13905  invss  13913  fullfunc  14030  fthfunc  14031  catccatid  14184  resscatc  14187  catcisolem  14188  catciso  14189  yoniso  14309  cntzrcl  15053  cntzssv  15054  ablfaclem3  15572  lmhmlsp  16052  resspsrbas  16405  resspsrvsca  16408  subrgpsr  16409  mplsubglem  16425  ressmplbas  16446  subrgmpl  16450  ressply1bas  16550  cssss  16835  basdif0  16941  ntrss2  17044  ordtbas2  17177  ordtbas  17178  cncls  17260  cmpfi  17393  kgentopon  17491  ptpjpre1  17524  xkoccn  17572  prdstopn  17581  uzfbas  17851  utoptop  18185  utopbas  18186  setsmstopn  18398  restmetu  18489  tngtopn  18562  iccntr  18723  metdstri  18752  pi1xfrcnvlem  18952  cphsubrglem  19011  tchcph  19065  ovolshftlem1  19272  ovolshft  19274  ovolscalem1  19276  ovolscalem2  19277  ovolsca  19278  uniioombllem2  19342  uniioombllem3a  19343  uniioombllem3  19344  uniioombllem4  19345  uniioombllem6  19347  itgioo  19574  limcnlp  19632  dvbsss  19656  dvcnvrelem1  19768  dvfsumle  19772  dvfsumabs  19774  mpfrcl  19806  pserdv  20212  rlimcnp2  20672  fsumharmonic  20717  chpval2  20869  nbgrassvt  21311  subgornss  21742  ocsh  22633  shsss  22663  speccl  23250  elnlfn  23279  pj3i  23559  sumdmdlem2  23770  ssnnssfz  23984  gsumpropd2lem  24049  dya2iocuni  24427  kur14lem1  24671  cvmliftmolem2  24748  cvmliftlem15  24764  trpredlem1  25254  wfrlem15  25294  comppfsc  26078  sdclem2  26137  sstotbnd2  26174  isbnd3  26184  diophin  26522  frlmplusgval  26898  frlmvscafval  26899  itgocn  27038  en2other2  27051  stoweidlem34  27451  stoweidlem59  27476  bnj1143  28499  bnj1262  28520  bnj517  28594  lkrlss  29210  pmapssat  29873  diass  31157  diaintclN  31173  dia2dimlem13  31191  dibintclN  31282  lcfrlem25  31682  lcdvbasess  31709  mapdin  31777
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
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 2374  df-cleq 2380  df-clel 2383  df-in 3270  df-ss 3277
  Copyright terms: Public domain W3C validator