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

Theorem ssbri 4730
 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 4729 . 2 (𝐴𝐵 → (𝐶𝐴𝐷𝐶𝐵𝐷))
31, 2ax-mp 5 1 (𝐶𝐴𝐷𝐶𝐵𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ⊆ wss 3607   class class class wbr 4685 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621  df-br 4686 This theorem is referenced by:  brel  5202  swoer  7817  swoord1  7818  swoord2  7819  ecopover  7894  endom  8024  brdom3  9388  brdom5  9389  brdom4  9390  fpwwe2lem13  9502  nqerf  9790  nqerrel  9792  isfull  16617  isfth  16621  fulloppc  16629  fthoppc  16630  fthsect  16632  fthinv  16633  fthmon  16634  fthepi  16635  ffthiso  16636  catcisolem  16803  psss  17261  efgrelex  18210  hlimadd  28178  hhsscms  28264  occllem  28290  nlelchi  29048  hmopidmchi  29138  fundmpss  31790  itg2gt0cn  33595  brresi  33643
 Copyright terms: Public domain W3C validator