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

Theorem ssrind 4036
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 4034 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  cin 3769  wss 3770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2778
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-v 3388  df-in 3777  df-ss 3784
This theorem is referenced by:  fictb  9356  isacs1i  16631  rescabs  16806  lsmdisj  18406  dmdprdsplit2lem  18759  obselocv  20396  restbas  21290  neitr  21312  restcls  21313  restntr  21314  nrmsep  21489  cldllycmp  21626  fclsneii  22148  tsmsres  22274  trcfilu  22425  metdseq0  22984  iundisj2  23656  uniioombllem3  23692  ppisval  25181  ppisval2  25182  chtwordi  25233  ppiwordi  25239  chpub  25296  chebbnd1lem1  25509  mdbr2  29679  mdslj1i  29702  mdsl2i  29705  mdslmd1lem1  29708  mdslmd3i  29715  mdexchi  29718  sumdmdlem  29801  iundisj2f  29919  iundisj2fi  30073  esumrnmpt2  30645  bnj1177  31590  sstotbnd2  34059  lcvexchlem5  35058  pnonsingN  35953  dochnoncon  37411  eldioph2lem2  38105  acsfn1p  38549  limsupres  40676  limsupresxr  40737  liminfresxr  40738  liminflelimsuplem  40746  rhmsscrnghm  42820  rngcresringcat  42824
  Copyright terms: Public domain W3C validator