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

Theorem ssrind 4199
Description: Add right intersection to subclass relation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
Hypothesis
Ref Expression
ssrind.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
ssrind (𝜑 → (𝐴𝐶) ⊆ (𝐵𝐶))

Proof of Theorem ssrind
StepHypRef Expression
1 ssrind.1 . 2 (𝜑𝐴𝐵)
2 ssrin 4197 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  cin 3913  wss 3914
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3449  df-in 3921  df-ss 3931
This theorem is referenced by:  fictb  10189  isacs1i  17545  rescabs  17726  rescabsOLD  17727  lsmdisj  19471  dmdprdsplit2lem  19832  acsfn1p  20309  obselocv  21157  restbas  22532  neitr  22554  restcls  22555  restntr  22556  nrmsep  22731  cldllycmp  22869  fclsneii  23391  tsmsres  23518  trcfilu  23669  metdseq0  24240  iundisj2  24936  uniioombllem3  24972  ppisval  26476  ppisval2  26477  chtwordi  26528  ppiwordi  26534  chpub  26591  chebbnd1lem1  26840  mdbr2  31287  mdslj1i  31310  mdsl2i  31313  mdslmd1lem1  31316  mdslmd3i  31323  mdexchi  31326  sumdmdlem  31409  iundisj2f  31561  iundisj2fi  31754  cycpmco2f1  32029  tocyccntz  32049  esumrnmpt2  32731  bnj1177  33682  sstotbnd2  36283  lcvexchlem5  37550  pnonsingN  38446  dochnoncon  39904  eldioph2lem2  41131  limsupres  44036  limsupresxr  44097  liminfresxr  44098  liminflelimsuplem  44106  rhmsscrnghm  46414  rngcresringcat  46418  ssdisjd  46982
  Copyright terms: Public domain W3C validator