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

Theorem ssbri 5188
Description: Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.)
Hypothesis
Ref Expression
ssbri.1 𝐴𝐵
Assertion
Ref Expression
ssbri (𝐶𝐴𝐷𝐶𝐵𝐷)

Proof of Theorem ssbri
StepHypRef Expression
1 ssbri.1 . 2 𝐴𝐵
2 ssbr 5187 . 2 (𝐴𝐵 → (𝐶𝐴𝐷𝐶𝐵𝐷))
31, 2ax-mp 5 1 (𝐶𝐴𝐷𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3951   class class class wbr 5143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2816  df-ss 3968  df-br 5144
This theorem is referenced by:  brel  5750  swoer  8776  swoord1  8777  swoord2  8778  ecopover  8861  endom  9019  brdom3  10568  brdom5  10569  brdom4  10570  fpwwe2lem12  10682  nqerf  10970  nqerrel  10972  isfull  17957  isfth  17961  fulloppc  17969  fthoppc  17970  fthsect  17972  fthinv  17973  fthmon  17974  fthepi  17975  ffthiso  17976  catcisolem  18155  psss  18625  efgrelex  19769  hlimadd  31212  hhsscms  31297  occllem  31322  nlelchi  32080  hmopidmchi  32170  fundmpss  35767  itg2gt0cn  37682  brresi2  37727  fullthinc2  49100  thincciso  49102
  Copyright terms: Public domain W3C validator