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

Theorem ssbri 4479
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 4478 . 2  |-  ( T. 
->  ( C A D  ->  C B D ) )
43trud 1392 1  |-  ( C A D  ->  C B D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   T. wtru 1384    C_ wss 3461   class class class wbr 4437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475  df-br 4438
This theorem is referenced by:  brel  5038  swoer  7341  swoord1  7342  swoord2  7343  ecopover  7417  endom  7544  brdom3  8909  brdom5  8910  brdom4  8911  fpwwe2lem13  9023  nqerf  9311  nqerrel  9313  isfull  15258  isfth  15262  fulloppc  15270  fthoppc  15271  fthsect  15273  fthinv  15274  fthmon  15275  fthepi  15276  ffthiso  15277  catcisolem  15412  psss  15823  efgrelex  16748  hlimadd  26088  hhsscms  26173  occllem  26199  nlelchi  26958  hmopidmchi  27048  fundmpss  29172  itg2gt0cn  30046  brresi  30185
  Copyright terms: Public domain W3C validator