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

Theorem ssbri 4256
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  |-  A  C_  B
Assertion
Ref Expression
ssbri  |-  ( C A D  ->  C B D )

Proof of Theorem ssbri
StepHypRef Expression
1 ssbri.1 . . . 4  |-  A  C_  B
21a1i 11 . . 3  |-  (  T. 
->  A  C_  B )
32ssbrd 4255 . 2  |-  (  T. 
->  ( C A D  ->  C B D ) )
43trud 1333 1  |-  ( C A D  ->  C B D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    T. wtru 1326    C_ wss 3322   class class class wbr 4214
This theorem is referenced by:  brel  4928  swoer  6935  swoord1  6936  swoord2  6937  ecopover  7010  endom  7136  brdom3  8408  brdom5  8409  brdom4  8410  fpwwe2lem13  8519  nqerf  8809  nqerrel  8811  isfull  14109  isfth  14113  fulloppc  14121  fthoppc  14122  fthsect  14124  fthinv  14125  fthmon  14126  fthepi  14127  ffthiso  14128  catcisolem  14263  psss  14648  efgrelex  15385  hlimadd  22697  hhsscms  22781  occllem  22807  nlelchi  23566  hmopidmchi  23656  fundmpss  25392  itg2gt0cn  26262  fnessref  26375  brresi  26422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336  df-br 4215
  Copyright terms: Public domain W3C validator