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

Theorem syl6eqss 3390
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 3374 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    C_ wss 3312
This theorem is referenced by:  syl6eqssr  3391  dmxpss  5292  dmsnopss  5334  iotassuni  5426  fvmptss  5805  fvmptss2  5816  fimacnv  5854  funressn  5911  frxp  6448  riotassuni  6580  oawordeulem  6789  omwordri  6807  oewordri  6827  map0e  7043  fodomr  7250  fipwuni  7423  fipwss  7426  ordtypelem6  7484  inf3lemd  7574  cantnfle  7618  cantnflem2  7638  ackbij1lem15  8106  ackbij2lem3  8113  cfub  8121  cflecard  8125  cfle  8126  fin23lem13  8204  fin23lem29  8213  compsscnvlem  8242  itunitc1  8292  fpwwe2lem12  8508  grur1a  8686  uzssz  10497  limsupgle  12263  isercolllem2  12451  isercoll  12453  fsumss  12511  sadcaddlem  12961  sadadd2lem  12963  sadadd3  12965  sadcl  12966  sadaddlem  12970  sadasslem  12974  sadeq  12976  smupvallem  12987  smucl  12988  prmreclem4  13279  prmreclem5  13280  1arith  13287  vdwmc2  13339  vdwlem13  13353  ramz2  13384  strfvss  13479  ressbasss  13513  prdsless  13677  sectss  13970  invss  13978  fullfunc  14095  fthfunc  14096  catccatid  14249  resscatc  14252  catcisolem  14253  catciso  14254  yoniso  14374  cntzrcl  15118  cntzssv  15119  ablfaclem3  15637  lmhmlsp  16117  resspsrbas  16470  resspsrvsca  16473  subrgpsr  16474  mplsubglem  16490  ressmplbas  16511  subrgmpl  16515  ressply1bas  16615  cssss  16904  basdif0  17010  ntrss2  17113  ordtbas2  17247  ordtbas  17248  cncls  17330  cmpfi  17463  kgentopon  17562  ptpjpre1  17595  xkoccn  17643  prdstopn  17652  uzfbas  17922  utoptop  18256  utopbas  18257  setsmstopn  18500  restmetu  18609  tngtopn  18683  iccntr  18844  metdstri  18873  pi1xfrcnvlem  19073  cphsubrglem  19132  tchcph  19186  ovolshftlem1  19397  ovolshft  19399  ovolscalem1  19401  ovolscalem2  19402  ovolsca  19403  uniioombllem2  19467  uniioombllem3a  19468  uniioombllem3  19469  uniioombllem4  19470  uniioombllem6  19472  itgioo  19699  limcnlp  19757  dvbsss  19781  dvcnvrelem1  19893  dvfsumle  19897  dvfsumabs  19899  mpfrcl  19931  pserdv  20337  rlimcnp2  20797  fsumharmonic  20842  chpval2  20994  nbgrassvt  21437  subgornss  21886  ocsh  22777  shsss  22807  speccl  23394  elnlfn  23423  pj3i  23703  sumdmdlem2  23914  ssnnssfz  24140  gsumpropd2lem  24212  inftmrel  24242  metidss  24278  dya2iocuni  24625  kur14lem1  24884  cvmliftmolem2  24961  cvmliftlem15  24977  trpredlem1  25497  wfrlem15  25544  mblfinlem  26234  comppfsc  26378  sdclem2  26437  sstotbnd2  26474  isbnd3  26484  diophin  26822  frlmplusgval  27197  frlmvscafval  27198  itgocn  27337  en2other2  27350  stoweidlem34  27750  stoweidlem59  27775  swrdltnd  28153  bnj1143  29098  bnj1262  29119  bnj517  29193  lkrlss  29830  pmapssat  30493  diass  31777  diaintclN  31793  dia2dimlem13  31811  dibintclN  31902  lcfrlem25  32302  lcdvbasess  32329  mapdin  32397
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator