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

Theorem syl6eqss 3394
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 3378 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  syl6eqssr  3395  dmxpss  5257  dmsnopss  5299  iotassuni  5385  fvmptss  5770  fvmptss2  5781  fimacnv  5823  funressn  5882  riotassuniOLD  6078  frxp  6671  suppssdm  6692  suppun  6698  suppss  6708  suppssov1  6710  suppss2  6712  suppssfv  6714  oawordeulem  6981  omwordri  6999  oewordri  7019  map0e  7238  fodomr  7450  fipwuni  7664  fipwss  7667  ordtypelem6  7725  inf3lemd  7821  cantnfle  7867  cantnflem2  7886  cantnfleOLD  7897  en2other2  8164  ackbij1lem15  8391  ackbij2lem3  8398  cfub  8406  cflecard  8410  cfle  8411  fin23lem13  8489  fin23lem29  8498  compsscnvlem  8527  itunitc1  8577  fpwwe2lem12  8796  grur1a  8974  uzssz  10868  swrdlend  12309  repswswrd  12406  limsupgle  12939  isercolllem2  13127  isercoll  13129  fsumss  13186  sadcaddlem  13636  sadadd2lem  13638  sadadd3  13640  sadcl  13641  sadaddlem  13645  sadasslem  13649  sadeq  13651  smupvallem  13662  smucl  13663  prmreclem4  13963  prmreclem5  13964  1arith  13971  vdwmc2  14023  vdwlem13  14037  ramz2  14068  strfvss  14175  ressbasss  14213  prdsless  14384  sectss  14674  invss  14682  fullfunc  14799  fthfunc  14800  catccatid  14953  resscatc  14956  catcisolem  14957  catciso  14958  yoniso  15078  cntzrcl  15825  cntzssv  15826  ablfaclem3  16562  lmhmlsp  17052  resspsrbas  17421  resspsrvsca  17424  subrgpsr  17425  mplsubglem  17444  mplsubglemOLD  17446  ressmplbas  17469  subrgmpl  17473  ressply1bas  17582  ply1coe  17643  evpmss  17858  cssss  17952  frlmplusgval  18033  frlmvscafval  18035  uvcresum  18060  basdif0  18400  ntrss2  18503  ordtbas2  18637  ordtbas  18638  cncls  18720  cmpfi  18853  kgentopon  18953  ptpjpre1  18986  xkoccn  19034  prdstopn  19043  uzfbas  19313  utoptop  19651  utopbas  19652  setsmstopn  19895  restmetu  20004  tngtopn  20078  iccntr  20240  metdstri  20269  pi1xfrcnvlem  20470  cphsubrglem  20538  tchcph  20594  rrxnm  20737  ovolshftlem1  20834  ovolshft  20836  ovolscalem1  20838  ovolscalem2  20839  ovolsca  20840  uniioombllem2  20905  uniioombllem3a  20906  uniioombllem3  20907  uniioombllem4  20908  uniioombllem6  20910  itgioo  21135  limcnlp  21195  dvbsss  21219  dvcnvrelem1  21331  dvfsumle  21335  dvfsumabs  21337  mpfrcl  21370  pserdv  21779  rlimcnp2  22245  fsumharmonic  22290  chpval2  22442  tglnssp  22865  nbgrassvt  23167  subgornss  23616  ocsh  24509  shsss  24539  speccl  25126  elnlfn  25155  pj3i  25435  sumdmdlem2  25646  ffsrn  25854  ssnnssfz  25899  inftmrel  26021  gsumpropd2lem  26093  metidss  26172  fsumcvg4  26234  dya2iocuni  26552  kur14lem1  26942  cvmliftmolem2  27019  cvmliftlem15  27035  trpredlem1  27538  wfrlem15  27585  mblfinlem2  28273  comppfsc  28423  sdclem2  28482  sstotbnd2  28517  isbnd3  28527  diophin  28956  itgocn  29366  stoweidlem34  29675  stoweidlem59  29700  clwwlksswrd  30286  mptscmfsuppd  30633  ply1coefsupp  30634  bnj1143  31486  bnj1262  31506  bnj517  31580  lkrlss  32313  pmapssat  32976  diass  34260  diaintclN  34276  dia2dimlem13  34294  dibintclN  34385  lcfrlem25  34785  lcdvbasess  34812  mapdin  34880
  Copyright terms: Public domain W3C validator