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

Theorem ssbri 4102
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 10 . . 3  |-  (  T. 
->  A  C_  B )
32ssbrd 4101 . 2  |-  (  T. 
->  ( C A D  ->  C B D ) )
43trud 1314 1  |-  ( C A D  ->  C B D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    T. wtru 1307    C_ wss 3186   class class class wbr 4060
This theorem is referenced by:  brel  4774  swoer  6730  swoord1  6731  swoord2  6732  ecopover  6805  endom  6931  brdom3  8198  brdom5  8199  brdom4  8200  fpwwe2lem13  8309  nqerf  8599  nqerrel  8601  isfull  13833  isfth  13837  fulloppc  13845  fthoppc  13846  fthsect  13848  fthinv  13849  fthmon  13850  fthepi  13851  ffthiso  13852  catcisolem  13987  psss  14372  efgrelex  15109  hlimadd  21827  hhsscms  21911  occllem  21937  nlelchi  22696  hmopidmchi  22786  fundmpss  24507  itg2gt0cn  25320  fnessref  25442  brresi  25532
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-in 3193  df-ss 3200  df-br 4061
  Copyright terms: Public domain W3C validator