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

Theorem ssrind 4216
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 4214 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  cin 3939  wss 3940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-in 3947  df-ss 3956
This theorem is referenced by:  fictb  9661  isacs1i  16923  rescabs  17098  lsmdisj  18743  dmdprdsplit2lem  19103  acsfn1p  19514  obselocv  20807  restbas  21701  neitr  21723  restcls  21724  restntr  21725  nrmsep  21900  cldllycmp  22038  fclsneii  22560  tsmsres  22686  trcfilu  22837  metdseq0  23396  iundisj2  24084  uniioombllem3  24120  ppisval  25614  ppisval2  25615  chtwordi  25666  ppiwordi  25672  chpub  25729  chebbnd1lem1  25978  mdbr2  30006  mdslj1i  30029  mdsl2i  30032  mdslmd1lem1  30035  mdslmd3i  30042  mdexchi  30045  sumdmdlem  30128  iundisj2f  30274  iundisj2fi  30452  cycpmco2f1  30699  tocyccntz  30719  esumrnmpt2  31232  bnj1177  32181  sstotbnd2  34939  lcvexchlem5  36060  pnonsingN  36955  dochnoncon  38413  eldioph2lem2  39242  limsupres  41870  limsupresxr  41931  liminfresxr  41932  liminflelimsuplem  41940  rhmsscrnghm  44199  rngcresringcat  44203
  Copyright terms: Public domain W3C validator