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

Theorem syl6eqss 3401
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 3385 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337
This theorem is referenced by:  syl6eqssr  3402  dmxpss  5264  dmsnopss  5306  iotassuni  5392  fvmptss  5777  fvmptss2  5788  fimacnv  5830  funressn  5890  riotassuniOLD  6084  frxp  6677  suppssdm  6698  suppun  6704  suppss  6714  suppssov1  6716  suppss2  6718  suppssfv  6720  oawordeulem  6985  omwordri  7003  oewordri  7023  map0e  7242  fodomr  7454  fipwuni  7668  fipwss  7671  ordtypelem6  7729  inf3lemd  7825  cantnfle  7871  cantnflem2  7890  cantnfleOLD  7901  en2other2  8168  ackbij1lem15  8395  ackbij2lem3  8402  cfub  8410  cflecard  8414  cfle  8415  fin23lem13  8493  fin23lem29  8502  compsscnvlem  8531  itunitc1  8581  fpwwe2lem12  8800  grur1a  8978  uzssz  10872  swrdlend  12317  repswswrd  12414  limsupgle  12947  isercolllem2  13135  isercoll  13137  fsumss  13194  sadcaddlem  13645  sadadd2lem  13647  sadadd3  13649  sadcl  13650  sadaddlem  13654  sadasslem  13658  sadeq  13660  smupvallem  13671  smucl  13672  prmreclem4  13972  prmreclem5  13973  1arith  13980  vdwmc2  14032  vdwlem13  14046  ramz2  14077  strfvss  14184  ressbasss  14222  prdsless  14393  sectss  14683  invss  14691  fullfunc  14808  fthfunc  14809  catccatid  14962  resscatc  14965  catcisolem  14966  catciso  14967  yoniso  15087  gsumpropd2lem  15496  cntzrcl  15836  cntzssv  15837  ablfaclem3  16578  lmhmlsp  17110  resspsrbas  17467  resspsrvsca  17470  subrgpsr  17471  mplsubglem  17490  mplsubglemOLD  17492  ressmplbas  17515  subrgmpl  17519  mpfrcl  17584  ressply1bas  17663  ply1coeOLD  17727  evpmss  17996  cssss  18090  frlmplusgval  18171  frlmvscafval  18173  uvcresum  18198  basdif0  18538  ntrss2  18641  ordtbas2  18775  ordtbas  18776  cncls  18858  cmpfi  18991  kgentopon  19091  ptpjpre1  19124  xkoccn  19172  prdstopn  19181  uzfbas  19451  utoptop  19789  utopbas  19790  setsmstopn  20033  restmetu  20142  tngtopn  20216  iccntr  20378  metdstri  20407  pi1xfrcnvlem  20608  cphsubrglem  20676  tchcph  20732  rrxnm  20875  ovolshftlem1  20972  ovolshft  20974  ovolscalem1  20976  ovolscalem2  20977  ovolsca  20978  uniioombllem2  21043  uniioombllem3a  21044  uniioombllem3  21045  uniioombllem4  21046  uniioombllem6  21048  itgioo  21273  limcnlp  21333  dvbsss  21357  dvcnvrelem1  21469  dvfsumle  21473  dvfsumabs  21475  pserdv  21874  rlimcnp2  22340  fsumharmonic  22385  chpval2  22537  tglnssp  22966  nbgrassvt  23312  subgornss  23761  ocsh  24654  shsss  24684  speccl  25271  elnlfn  25300  pj3i  25580  sumdmdlem2  25791  ffsrn  25997  ssnnssfz  26044  inftmrel  26165  metidss  26287  fsumcvg4  26349  dya2iocuni  26667  kur14lem1  27063  cvmliftmolem2  27140  cvmliftlem15  27156  trpredlem1  27660  wfrlem15  27707  mblfinlem2  28400  comppfsc  28550  sdclem2  28609  sstotbnd2  28644  isbnd3  28654  diophin  29082  itgocn  29492  stoweidlem34  29800  stoweidlem59  29825  clwwlksswrd  30411  ssnn0ssfz  30711  fsuppmapnn0fiublem  30767  fsuppmapnn0fiub  30768  bnj1143  31713  bnj1262  31733  bnj517  31807  lkrlss  32633  pmapssat  33296  diass  34580  diaintclN  34596  dia2dimlem13  34614  dibintclN  34705  lcfrlem25  35105  lcdvbasess  35132  mapdin  35200
  Copyright terms: Public domain W3C validator