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

Theorem ssbri 4065
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 4064 . 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 3152   class class class wbr 4023
This theorem is referenced by:  brel  4737  swoer  6688  swoord1  6689  swoord2  6690  ecopover  6762  endom  6888  brdom3  8153  brdom5  8154  brdom4  8155  fpwwe2lem13  8264  nqerf  8554  nqerrel  8556  isfull  13784  isfth  13788  fulloppc  13796  fthoppc  13797  fthsect  13799  fthinv  13800  fthmon  13801  fthepi  13802  ffthiso  13803  catcisolem  13938  psss  14323  efgrelex  15060  hlimadd  21772  hhsscms  21856  occllem  21882  nlelchi  22641  hmopidmchi  22731  fundmpss  24122  fnessref  26293  brresi  26383
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166  df-br 4024
  Copyright terms: Public domain W3C validator