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

Theorem ssbri 4458
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 4457 . 2  |-  ( T. 
->  ( C A D  ->  C B D ) )
43trud 1463 1  |-  ( C A D  ->  C B D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   T. wtru 1455    C_ wss 3415   class class class wbr 4415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-in 3422  df-ss 3429  df-br 4416
This theorem is referenced by:  brel  4901  swoer  7416  swoord1  7417  swoord2  7418  ecopover  7492  endom  7621  brdom3  8981  brdom5  8982  brdom4  8983  fpwwe2lem13  9092  nqerf  9380  nqerrel  9382  isfull  15863  isfth  15867  fulloppc  15875  fthoppc  15876  fthsect  15878  fthinv  15879  fthmon  15880  fthepi  15881  ffthiso  15882  catcisolem  16049  psss  16508  efgrelex  17449  hlimadd  26894  hhsscms  26978  occllem  27004  nlelchi  27762  hmopidmchi  27852  fundmpss  30455  itg2gt0cn  32041  brresi  32089
  Copyright terms: Public domain W3C validator