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

Theorem ssrind 4209
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 4207 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  cin 3932  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-in 3940  df-ss 3949
This theorem is referenced by:  fictb  9655  isacs1i  16916  rescabs  17091  lsmdisj  18736  dmdprdsplit2lem  19096  acsfn1p  19507  obselocv  20800  restbas  21694  neitr  21716  restcls  21717  restntr  21718  nrmsep  21893  cldllycmp  22031  fclsneii  22553  tsmsres  22679  trcfilu  22830  metdseq0  23389  iundisj2  24077  uniioombllem3  24113  ppisval  25608  ppisval2  25609  chtwordi  25660  ppiwordi  25666  chpub  25723  chebbnd1lem1  25972  mdbr2  30000  mdslj1i  30023  mdsl2i  30026  mdslmd1lem1  30029  mdslmd3i  30036  mdexchi  30039  sumdmdlem  30122  iundisj2f  30268  iundisj2fi  30446  cycpmco2f1  30693  tocyccntz  30713  esumrnmpt2  31226  bnj1177  32175  sstotbnd2  34933  lcvexchlem5  36054  pnonsingN  36949  dochnoncon  38407  eldioph2lem2  39236  limsupres  41862  limsupresxr  41923  liminfresxr  41924  liminflelimsuplem  41932  rhmsscrnghm  44225  rngcresringcat  44229
  Copyright terms: Public domain W3C validator