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

Theorem ssbri 5107
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 5106 . 2 (𝐴𝐵 → (𝐶𝐴𝐷𝐶𝐵𝐷))
31, 2ax-mp 5 1 (𝐶𝐴𝐷𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3939   class class class wbr 5062
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 2797
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 2804  df-cleq 2818  df-clel 2897  df-in 3946  df-ss 3955  df-br 5063
This theorem is referenced by:  brel  5615  swoer  8312  swoord1  8313  swoord2  8314  ecopover  8394  endom  8528  brdom3  9942  brdom5  9943  brdom4  9944  fpwwe2lem13  10056  nqerf  10344  nqerrel  10346  isfull  17173  isfth  17177  fulloppc  17185  fthoppc  17186  fthsect  17188  fthinv  17189  fthmon  17190  fthepi  17191  ffthiso  17192  catcisolem  17359  psss  17817  efgrelex  18800  hlimadd  28887  hhsscms  28972  occllem  28997  nlelchi  29755  hmopidmchi  29845  fundmpss  32896  itg2gt0cn  34817  brresi2  34865
  Copyright terms: Public domain W3C validator