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

Theorem ssbrd 4328
Description: Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.)
Hypothesis
Ref Expression
ssbrd.1  |-  ( ph  ->  A  C_  B )
Assertion
Ref Expression
ssbrd  |-  ( ph  ->  ( C A D  ->  C B D ) )

Proof of Theorem ssbrd
StepHypRef Expression
1 ssbrd.1 . . 3  |-  ( ph  ->  A  C_  B )
21sseld 3350 . 2  |-  ( ph  ->  ( <. C ,  D >.  e.  A  ->  <. C ,  D >.  e.  B ) )
3 df-br 4288 . 2  |-  ( C A D  <->  <. C ,  D >.  e.  A )
4 df-br 4288 . 2  |-  ( C B D  <->  <. C ,  D >.  e.  B )
52, 3, 43imtr4g 270 1  |-  ( ph  ->  ( C A D  ->  C B D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756    C_ wss 3323   <.cop 3878   class class class wbr 4287
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 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337  df-br 4288
This theorem is referenced by:  ssbri  4329  sess1  4683  brrelex12  4871  coss1  4990  coss2  4991  eqbrrdva  5004  ersym  7105  ertr  7108  fpwwe2lem6  8794  fpwwe2lem7  8795  fpwwe2lem9  8797  fpwwe2lem12  8800  fpwwe2lem13  8801  fpwwe2  8802  fthres2  14834  invfuc  14876  pospo  15135  dirref  15397  efgcpbl  16244  frgpuplem  16260  subrguss  16858  znleval  17962  ustref  19768  ustuqtop4  19794  isucn2  19829  brelg  25892  metider  26273  fundmpss  27528
  Copyright terms: Public domain W3C validator