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

Theorem ssbri 4657
 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 . . . 4 𝐴𝐵
21a1i 11 . . 3 (⊤ → 𝐴𝐵)
32ssbrd 4656 . 2 (⊤ → (𝐶𝐴𝐷𝐶𝐵𝐷))
43trud 1490 1 (𝐶𝐴𝐷𝐶𝐵𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ⊤wtru 1481   ⊆ wss 3555   class class class wbr 4613 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3562  df-ss 3569  df-br 4614 This theorem is referenced by:  brel  5128  swoer  7717  swoord1  7718  swoord2  7719  ecopover  7796  ecopoverOLD  7797  endom  7926  brdom3  9294  brdom5  9295  brdom4  9296  fpwwe2lem13  9408  nqerf  9696  nqerrel  9698  isfull  16491  isfth  16495  fulloppc  16503  fthoppc  16504  fthsect  16506  fthinv  16507  fthmon  16508  fthepi  16509  ffthiso  16510  catcisolem  16677  psss  17135  efgrelex  18085  hlimadd  27896  hhsscms  27982  occllem  28008  nlelchi  28766  hmopidmchi  28856  fundmpss  31365  itg2gt0cn  33094  brresi  33142
 Copyright terms: Public domain W3C validator