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

Theorem syl6eqss 3549
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 3533 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1395    C_ wss 3471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3478  df-ss 3485
This theorem is referenced by:  syl6eqssr  3550  dmxpss  5445  dmsnopss  5486  iotassuni  5573  fvmptss  5965  fvmptss2  5976  fimacnv  6020  funressn  6085  riotassuniOLD  6294  frxp  6909  suppssdm  6930  suppun  6938  suppss  6948  suppssov1  6950  suppss2  6952  suppssfv  6954  oawordeulem  7221  omwordri  7239  oewordri  7259  fodomr  7687  fipwuni  7904  fipwss  7907  ordtypelem6  7966  inf3lemd  8061  cantnfle  8107  cantnflem2  8126  cantnfleOLD  8137  en2other2  8404  ackbij1lem15  8631  ackbij2lem3  8638  cfub  8646  cflecard  8650  cfle  8651  fin23lem13  8729  fin23lem29  8738  compsscnvlem  8767  itunitc1  8817  fpwwe2lem12  9036  grur1a  9214  uzssz  11125  fsuppmapnn0fiublem  12099  fsuppmapnn0fiub  12100  swrdlend  12667  repswswrd  12768  limsupgle  13312  isercolllem2  13500  isercoll  13502  fsumss  13559  sadcaddlem  14119  sadadd2lem  14121  sadadd3  14123  sadcl  14124  sadaddlem  14128  sadasslem  14132  sadeq  14134  smupvallem  14145  smucl  14146  prmreclem4  14449  prmreclem5  14450  1arith  14457  vdwmc2  14509  vdwlem13  14523  ramz2  14554  strfvss  14662  ressbasss  14703  prdsless  14880  sectss  15168  invss  15177  fullfunc  15322  fthfunc  15323  catccatid  15508  resscatc  15511  catcisolem  15512  catciso  15513  yoniso  15681  gsumpropd2lem  16027  cntzrcl  16492  cntzssv  16493  gsumzmhm  17084  ablfaclem3  17265  lmhmlsp  17822  resspsrbas  18197  resspsrvsca  18200  subrgpsr  18201  mplsubglem  18220  mplsubglemOLD  18222  ressmplbas  18245  subrgmpl  18249  mpfrcl  18314  ressply1bas  18397  ply1coeOLD  18465  evpmss  18749  cssss  18843  frlmplusgval  18924  frlmvscafval  18926  uvcresum  18951  scmatlss  19154  cpmatsubgpmat  19348  basdif0  19581  ntrss2  19685  ordtbas2  19819  ordtbas  19820  cncls  19902  cmpfi  20035  comppfsc  20159  kgentopon  20165  ptpjpre1  20198  xkoccn  20246  prdstopn  20255  uzfbas  20525  utoptop  20863  utopbas  20864  setsmstopn  21107  restmetu  21216  tngtopn  21290  iccntr  21452  metdstri  21481  pi1xfrcnvlem  21682  cphsubrglem  21750  tchcph  21806  rrxnm  21949  ovolshftlem1  22046  ovolshft  22048  ovolscalem1  22050  ovolscalem2  22051  ovolsca  22052  uniioombllem2  22118  uniioombllem3a  22119  uniioombllem3  22120  uniioombllem4  22121  uniioombllem6  22123  itgioo  22348  limcnlp  22408  dvbsss  22432  dvcnvrelem1  22544  dvfsumle  22548  dvfsumabs  22550  pserdv  22950  rlimcnp2  23422  fsumharmonic  23467  chpval2  23619  tglnssp  24065  perpln1  24213  perpln2  24214  nbgrassvt  24560  clwwlksswrd  24904  subgornss  25435  ocsh  26328  shsss  26358  speccl  26945  elnlfn  26974  pj3i  27254  sumdmdlem2  27465  fcoinver  27602  ffsrn  27709  ssnnssfz  27757  inftmrel  27884  metidss  28031  fsumcvg4  28093  dya2iocuni  28427  carsgcl  28448  kur14lem1  28847  cvmliftmolem2  28924  cvmliftlem15  28940  mrsubrn  29070  msubrn  29086  relexpnndm  29266  trpredlem1  29527  wfrlem15  29574  mblfinlem2  30257  sdclem2  30440  sstotbnd2  30475  isbnd3  30485  diophin  30911  itgocn  31317  ibliooicc  31973  stoweidlem34  32019  stoweidlem59  32044  etransclem24  32244  rnghmresfn  32915  rnghmsscmap2  32925  rnghmsscmap  32926  rngchomrnghmresOLD  32948  funcrngcsetc  32950  rhmresfn  32961  dfringc2  32970  rhmsscmap2  32971  rhmsscmap  32972  rhmsscrnghm  32978  funcringcsetc  32987  funcringcsetcOLD2lem9  32996  rngcrescrhm  33037  rhmsubclem1  33038  rhmsubclem4  33041  rngcrescrhmOLD  33056  rhmsubcOLDlem1  33057  ssnn0ssfz  33082  bnj1143  33992  bnj1262  34012  bnj517  34086  lkrlss  34963  pmapssat  35626  diass  36912  diaintclN  36928  dia2dimlem13  36946  dibintclN  37037  lcfrlem25  37437  lcdvbasess  37464  mapdin  37532  xptrrel  37935
  Copyright terms: Public domain W3C validator