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

Theorem syl6eqss 3482
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 3466 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1444    C_ wss 3404
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-in 3411  df-ss 3418
This theorem is referenced by:  syl6eqssr  3483  dmxpss  5268  dmsnopss  5308  iotassuni  5562  fvmptss  5958  fvmptss2  5969  fimacnv  6012  funressn  6077  riotassuni  6288  frxp  6906  suppssdm  6927  suppun  6935  suppss  6945  suppssov1  6947  suppss2  6949  suppssfv  6951  wfrlem15  7050  oawordeulem  7255  omwordri  7273  oewordri  7293  fodomr  7723  fipwuni  7940  fipwss  7943  ordtypelem6  8038  inf3lemd  8132  cantnfle  8176  cantnflem2  8195  en2other2  8440  ackbij1lem15  8664  ackbij2lem3  8671  cfub  8679  cflecard  8683  cfle  8684  fin23lem13  8762  fin23lem29  8771  compsscnvlem  8800  itunitc1  8850  fpwwe2lem12  9066  grur1a  9244  uzssz  11178  fsuppmapnn0fiublem  12202  fsuppmapnn0fiub  12203  swrdlend  12787  repswswrd  12887  xptrrel  13044  relexpnndm  13104  limsupgle  13535  isercolllem2  13729  isercoll  13731  fsumss  13791  sadcaddlem  14431  sadadd2lem  14433  sadadd3  14435  sadcl  14436  sadaddlem  14440  sadasslem  14444  sadeq  14446  smupvallem  14457  smucl  14458  prmreclem4  14863  prmreclem5  14864  1arith  14871  vdwmc2  14929  vdwlem13  14943  ramz2  14982  strfvss  15139  ressbasss  15181  prdsless  15361  sectss  15657  invss  15666  fullfunc  15811  fthfunc  15812  catccatid  15997  resscatc  16000  catcisolem  16001  catciso  16002  yoniso  16170  gsumpropd2lem  16516  cntzrcl  16981  cntzssv  16982  gsumzmhm  17570  ablfaclem3  17720  lmhmlsp  18272  resspsrbas  18639  resspsrvsca  18642  subrgpsr  18643  mplsubglem  18658  ressmplbas  18680  subrgmpl  18684  mpfrcl  18741  ressply1bas  18822  ply1coeOLD  18890  evpmss  19154  cssss  19248  frlmplusgval  19326  frlmvscafval  19328  uvcresum  19351  scmatlss  19550  cpmatsubgpmat  19744  basdif0  19968  ntrss2  20072  ordtbas2  20207  ordtbas  20208  cncls  20290  cmpfi  20423  comppfsc  20547  kgentopon  20553  ptpjpre1  20586  xkoccn  20634  prdstopn  20643  uzfbas  20913  utoptop  21249  utopbas  21250  setsmstopn  21493  restmetu  21585  tngtopn  21658  iccntr  21839  metdstri  21868  metdstriOLD  21883  pi1xfrcnvlem  22087  cphsubrglem  22155  tchcph  22211  rrxnm  22350  ovolshftlem1  22462  ovolshft  22464  ovolscalem1  22466  ovolscalem2  22467  ovolsca  22468  uniioombllem2  22540  uniioombllem2OLD  22541  uniioombllem3a  22542  uniioombllem3  22543  uniioombllem4  22544  uniioombllem6  22546  itgioo  22773  limcnlp  22833  dvbsss  22857  dvcnvrelem1  22969  dvfsumle  22973  dvfsumabs  22975  pserdv  23384  rlimcnp2  23892  fsumharmonic  23937  chpval2  24146  tglnssp  24597  perpln1  24755  perpln2  24756  nbgrassvt  25161  clwwlksswrd  25505  subgornss  26034  ocsh  26936  shsss  26966  speccl  27552  elnlfn  27581  pj3i  27861  sumdmdlem2  28072  fcoinver  28214  ffsrn  28314  ssnnssfz  28367  inftmrel  28497  smatrcl  28622  metidss  28694  fsumcvg4  28756  dya2iocuni  29105  carsgcl  29136  bnj1143  29602  bnj1262  29622  bnj517  29696  kur14lem1  29929  cvmliftmolem2  30005  cvmliftlem15  30021  mrsubrn  30151  msubrn  30167  trpredlem1  30468  poimirlem30  31970  mblfinlem2  31978  sdclem2  32071  sstotbnd2  32106  isbnd3  32116  lkrlss  32661  pmapssat  33324  diass  34610  diaintclN  34626  dia2dimlem13  34644  dibintclN  34735  lcfrlem25  35135  lcdvbasess  35162  mapdin  35230  diophin  35615  itgocn  36030  relexp0a  36308  frege131d  36356  fsumsupp0  37657  ibliooicc  37848  stoweidlem34  37895  stoweidlem59  37920  etransclem24  38123  caratheodory  38349  ovnhoilem1  38423  hspdifhsp  38438  uhgrspansubgr  39363  rnghmresfn  40018  rnghmsscmap2  40028  rnghmsscmap  40029  rngchomrnghmresALTV  40051  funcrngcsetc  40053  rhmresfn  40064  dfringc2  40073  rhmsscmap2  40074  rhmsscmap  40075  rhmsscrnghm  40081  funcringcsetc  40090  funcringcsetcALTV2lem9  40099  rngcrescrhm  40140  rhmsubclem1  40141  rhmsubclem4  40144  rngcrescrhmALTV  40159  rhmsubcALTVlem1  40160  ssnn0ssfz  40183
  Copyright terms: Public domain W3C validator