Theorem syl6eqss 3655

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

Step	Hyp	Ref	Expression
1		syl6eqss.1	. 2 |- ( ph -> A = B )
2		syl6eqss.2	. . 3 |- B C_ C
3	2	a1i 11	. 2 |- ( ph -> B C_ C )
4	1, 3	eqsstrd 3639	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  syl6eqssr  3656  dmxpss  5565  dmsnopss  5607  iotassuni  5867  fvmptss  6292  fvmptss2  6304  fimacnv  6347  funressn  6426  riotassuni  6648  frxp  7287  suppssdm  7308  suppun  7315  suppss  7325  suppssov1  7327  suppss2  7329  suppssfv  7331  wfrlem15  7429  oawordeulem  7634  omwordri  7652  oewordri  7672  fodomr  8111  fipwuni  8332  fipwss  8335  ordtypelem6  8428  inf3lemd  8524  cantnfle  8568  cantnflem2  8587  en2other2  8832  ackbij1lem15  9056  ackbij2lem3  9063  cfub  9071  cflecard  9075  cfle  9076  fin23lem13  9154  fin23lem29  9163  compsscnvlem  9192  itunitc1  9242  fpwwe2lem12  9463  grur1a  9641  uzssz  11707  fsuppmapnn0fiublem  12789  fsuppmapnn0fiub  12790  fsuppmapnn0fiubOLD  12791  swrdlend  13431  repswswrd  13531  cshimadifsn  13575  xptrrel  13719  relexpnndm  13781  limsupgle  14208  isercolllem2  14396  isercoll  14398  fsumss  14456  sadcaddlem  15179  sadadd2lem  15181  sadadd3  15183  sadcl  15184  sadaddlem  15188  sadasslem  15192  sadeq  15194  smupvallem  15205  smucl  15206  prmreclem4  15623  prmreclem5  15624  1arith  15631  vdwmc2  15683  vdwlem13  15697  ramz2  15728  strfvss  15880  ressbasss  15932  prdsless  16123  sectss  16412  invss  16421  fullfunc  16566  fthfunc  16567  catccatid  16752  resscatc  16755  catcisolem  16756  catciso  16757  yoniso  16925  gsumpropd2lem  17273  cntzrcl  17760  cntzssv  17761  gsumzmhm  18337  ablfaclem3  18486  lmhmlsp  19049  resspsrbas  19415  resspsrvsca  19418  subrgpsr  19419  mplsubglem  19434  ressmplbas  19456  subrgmpl  19460  mpfrcl  19518  ressply1bas  19599  evpmss  19932  cssss  20029  frlmplusgval  20107  frlmvscafval  20109  uvcresum  20132  scmatlss  20331  cpmatsubgpmat  20525  toponsspwpw  20726  basdif0  20757  ntrss2  20861  ordtbas2  20995  ordtbas  20996  cncls  21078  cmpfi  21211  comppfsc  21335  kgentopon  21341  ptpjpre1  21374  xkoccn  21422  prdstopn  21431  uzfbas  21702  utoptop  22038  utopbas  22039  setsmstopn  22283  restmetu  22375  tngtopn  22454  iccntr  22624  metdstri  22654  pi1xfrcnvlem  22856  cphsubrglem  22977  tchcph  23036  rrxnm  23179  ovolshftlem1  23277  ovolshft  23279  ovolscalem1  23281  ovolscalem2  23282  ovolsca  23283  uniioombllem2  23351  uniioombllem3a  23352  uniioombllem3  23353  uniioombllem4  23354  uniioombllem6  23356  itgioo  23582  limcnlp  23642  dvbsss  23666  dvcnvrelem1  23780  dvfsumle  23784  dvfsumabs  23786  pserdv  24183  rlimcnp2  24693  fsumharmonic  24738  chpval2  24943  tglnssp  25447  perpln1  25605  perpln2  25606  uhgrspansubgr  26183  ocsh  28142  shsss  28172  speccl  28758  elnlfn  28787  pj3i  29067  sumdmdlem2  29278  fcoinver  29418  ffsrn  29504  ssnnssfz  29549  inftmrel  29734  smatrcl  29862  metidss  29934  fsumcvg4  29996  dya2iocuni  30345  carsgcl  30366  breprexplema  30708  bnj1143  30861  bnj1262  30881  bnj517  30955  kur14lem1  31188  cvmliftmolem2  31264  cvmliftlem15  31280  mrsubrn  31410  msubrn  31426  trpredlem1  31727  bj-ismooredr2  33065  poimirlem30  33439  mblfinlem2  33447  sdclem2  33538  sstotbnd2  33573  isbnd3  33583  lkrlss  34382  pmapssat  35045  diass  36331  diaintclN  36347  dia2dimlem13  36365  dibintclN  36456  lcfrlem25  36856  lcdvbasess  36883  mapdin  36951  diophin  37336  itgocn  37734  relexp0a  38008  frege131d  38056  fsovrfovd  38303  clsk1indlem2  38340  clsk1indlem3  38341  unirestss  39307  fsumsupp0  39810  limsupequzlem  39954  ibliooicc  40187  stoweidlem34  40251  stoweidlem59  40276  etransclem24  40475  caratheodory  40742  ovnhoilem1  40815  hspdifhsp  40830  smfaddlem2  40972  smflimlem1  40979  smflimlem2  40980  smfmullem4  41001  smfsuplem1  41017  rnghmresfn  41963  rnghmsscmap2  41973  rnghmsscmap  41974  rngchomrnghmresALTV  41996  funcrngcsetc  41998  rhmresfn  42009  dfringc2  42018  rhmsscmap2  42019  rhmsscmap  42020  rhmsscrnghm  42026  funcringcsetc  42035  funcringcsetcALTV2lem9  42044  rngcrescrhm  42085  rhmsubclem1  42086  rhmsubclem4  42089  rngcrescrhmALTV  42103  rhmsubcALTVlem1  42104  ssnn0ssfz  42127  setrec2fun  42439