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

Theorem ssbri 4355
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 4354 . 2  |-  ( T. 
->  ( C A D  ->  C B D ) )
43trud 1378 1  |-  ( C A D  ->  C B D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   T. wtru 1370    C_ wss 3349   class class class wbr 4313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3356  df-ss 3363  df-br 4314
This theorem is referenced by:  brel  4908  swoer  7150  swoord1  7151  swoord2  7152  ecopover  7225  endom  7357  brdom3  8716  brdom5  8717  brdom4  8718  fpwwe2lem13  8830  nqerf  9120  nqerrel  9122  isfull  14841  isfth  14845  fulloppc  14853  fthoppc  14854  fthsect  14856  fthinv  14857  fthmon  14858  fthepi  14859  ffthiso  14860  catcisolem  14995  psss  15405  efgrelex  16269  hlimadd  24617  hhsscms  24702  occllem  24728  nlelchi  25487  hmopidmchi  25577  fundmpss  27599  itg2gt0cn  28473  fnessref  28591  brresi  28638
  Copyright terms: Public domain W3C validator