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

Theorem ssrind 4198
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 4196 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
31, 2syl 18 1 (𝜑 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  cin 3906  wss 3907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737
This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3914  df-ss 3924
This theorem is referenced by:  fictb  10215  isacs1i  17703  rescabs  17880  lsmdisj  19742  dmdprdsplit2lem  20108  rhmsscrnghm  20741  rngcresringcat  20745  acsfn1p  20871  obselocv  21838  restbas  23276  neitr  23298  restcls  23299  restntr  23300  nrmsep  23475  cldllycmp  23613  fclsneii  24135  tsmsres  24262  trcfilu  24411  metdseq0  24973  iundisj2  25669  uniioombllem3  25705  ppisval  27226  ppisval2  27227  chtwordi  27278  ppiwordi  27284  chpub  27342  chebbnd1lem1  27591  mdbr2  32557  mdslj1i  32580  mdsl2i  32583  mdslmd1lem1  32586  mdslmd3i  32593  mdexchi  32596  sumdmdlem  32679  iundisj2f  32845  iundisj2fi  33054  cycpmco2f1  33357  tocyccntz  33377  esumrnmpt2  34375  bnj1177  35311  sstotbnd2  38285  lcvexchlem5  39674  pnonsingN  40569  dochnoncon  42027  eldioph2lem2  43354  limsupres  46277  limsupresxr  46338  liminfresxr  46339  liminflelimsuplem  46347  ssdisjd  49437
  Copyright terms: Public domain W3C validator