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

Theorem ssbri 5194
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 5193 . 2 (𝐴𝐵 → (𝐶𝐴𝐷𝐶𝐵𝐷))
31, 2ax-mp 5 1 (𝐶𝐴𝐷𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3944   class class class wbr 5149
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 1905  ax-6 1963  ax-7 2003  ax-8 2100
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-clel 2802  df-ss 3961  df-br 5150
This theorem is referenced by:  brel  5743  swoer  8755  swoord1  8756  swoord2  8757  ecopover  8840  endom  9000  brdom3  10553  brdom5  10554  brdom4  10555  fpwwe2lem12  10667  nqerf  10955  nqerrel  10957  isfull  17902  isfth  17906  fulloppc  17914  fthoppc  17915  fthsect  17917  fthinv  17918  fthmon  17919  fthepi  17920  ffthiso  17921  catcisolem  18102  psss  18575  efgrelex  19718  hlimadd  31075  hhsscms  31160  occllem  31185  nlelchi  31943  hmopidmchi  32033  fundmpss  35493  itg2gt0cn  37279  brresi2  37324  fullthinc2  48239  thincciso  48241
  Copyright terms: Public domain W3C validator