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

Theorem syl6eqss 3547
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 3531 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1374    C_ wss 3469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-in 3476  df-ss 3483
This theorem is referenced by:  syl6eqssr  3548  dmxpss  5429  dmsnopss  5471  iotassuni  5558  fvmptss  5949  fvmptss2  5960  fimacnv  6004  funressn  6065  riotassuniOLD  6273  frxp  6883  suppssdm  6904  suppun  6910  suppss  6920  suppssov1  6922  suppss2  6924  suppssfv  6926  oawordeulem  7193  omwordri  7211  oewordri  7231  map0e  7446  fodomr  7658  fipwuni  7875  fipwss  7878  ordtypelem6  7937  inf3lemd  8033  cantnfle  8079  cantnflem2  8098  cantnfleOLD  8109  en2other2  8376  ackbij1lem15  8603  ackbij2lem3  8610  cfub  8618  cflecard  8622  cfle  8623  fin23lem13  8701  fin23lem29  8710  compsscnvlem  8739  itunitc1  8789  fpwwe2lem12  9008  grur1a  9186  uzssz  11090  fsuppmapnn0fiublem  12052  fsuppmapnn0fiub  12053  swrdlend  12606  repswswrd  12706  limsupgle  13249  isercolllem2  13437  isercoll  13439  fsumss  13496  sadcaddlem  13955  sadadd2lem  13957  sadadd3  13959  sadcl  13960  sadaddlem  13964  sadasslem  13968  sadeq  13970  smupvallem  13981  smucl  13982  prmreclem4  14285  prmreclem5  14286  1arith  14293  vdwmc2  14345  vdwlem13  14359  ramz2  14390  strfvss  14497  ressbasss  14536  prdsless  14707  sectss  14997  invss  15005  fullfunc  15122  fthfunc  15123  catccatid  15276  resscatc  15279  catcisolem  15280  catciso  15281  yoniso  15401  gsumpropd2lem  15811  cntzrcl  16153  cntzssv  16154  ablfaclem3  16921  lmhmlsp  17471  resspsrbas  17834  resspsrvsca  17837  subrgpsr  17838  mplsubglem  17857  mplsubglemOLD  17859  ressmplbas  17882  subrgmpl  17886  mpfrcl  17951  ressply1bas  18034  ply1coeOLD  18102  evpmss  18382  cssss  18476  frlmplusgval  18557  frlmvscafval  18559  uvcresum  18584  scmatlss  18787  cpmatsubgpmat  18981  basdif0  19214  ntrss2  19317  ordtbas2  19451  ordtbas  19452  cncls  19534  cmpfi  19667  kgentopon  19767  ptpjpre1  19800  xkoccn  19848  prdstopn  19857  uzfbas  20127  utoptop  20465  utopbas  20466  setsmstopn  20709  restmetu  20818  tngtopn  20892  iccntr  21054  metdstri  21083  pi1xfrcnvlem  21284  cphsubrglem  21352  tchcph  21408  rrxnm  21551  ovolshftlem1  21648  ovolshft  21650  ovolscalem1  21652  ovolscalem2  21653  ovolsca  21654  uniioombllem2  21720  uniioombllem3a  21721  uniioombllem3  21722  uniioombllem4  21723  uniioombllem6  21725  itgioo  21950  limcnlp  22010  dvbsss  22034  dvcnvrelem1  22146  dvfsumle  22150  dvfsumabs  22152  pserdv  22551  rlimcnp2  23017  fsumharmonic  23062  chpval2  23214  tglnssp  23660  perpln1  23788  perpln2  23789  nbgrassvt  24095  clwwlksswrd  24439  subgornss  24834  ocsh  25727  shsss  25757  speccl  26344  elnlfn  26373  pj3i  26653  sumdmdlem2  26864  fcoinver  26983  ffsrn  27074  ssnnssfz  27115  inftmrel  27236  metidss  27356  fsumcvg4  27418  dya2iocuni  27744  kur14lem1  28140  cvmliftmolem2  28217  cvmliftlem15  28233  trpredlem1  28737  wfrlem15  28784  mblfinlem2  29480  comppfsc  29630  sdclem2  29689  sstotbnd2  29724  isbnd3  29734  diophin  30161  itgocn  30571  stoweidlem34  31153  stoweidlem59  31178  ssnn0ssfz  31877  bnj1143  32803  bnj1262  32823  bnj517  32897  lkrlss  33767  pmapssat  34430  diass  35714  diaintclN  35730  dia2dimlem13  35748  dibintclN  35839  lcfrlem25  36239  lcdvbasess  36266  mapdin  36334  xptrrel  36660
  Copyright terms: Public domain W3C validator