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

Theorem ssbrd 4444
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 3431 . 2  |-  ( ph  ->  ( <. C ,  D >.  e.  A  ->  <. C ,  D >.  e.  B ) )
3 df-br 4403 . 2  |-  ( C A D  <->  <. C ,  D >.  e.  A )
4 df-br 4403 . 2  |-  ( C B D  <->  <. C ,  D >.  e.  B )
52, 3, 43imtr4g 274 1  |-  ( ph  ->  ( C A D  ->  C B D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1887    C_ wss 3404   <.cop 3974   class class class wbr 4402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-in 3411  df-ss 3418  df-br 4403
This theorem is referenced by:  ssbri  4445  sess1  4802  brrelex12  4872  coss1  4990  coss2  4991  eqbrrdva  5004  ersym  7375  ertr  7378  fpwwe2lem6  9060  fpwwe2lem7  9061  fpwwe2lem9  9063  fpwwe2lem12  9066  fpwwe2lem13  9067  fpwwe2  9068  coss12d  13036  fthres2  15837  invfuc  15879  pospo  16219  dirref  16481  efgcpbl  17406  frgpuplem  17422  subrguss  18023  znleval  19125  ustref  21233  ustuqtop4  21259  isucn2  21294  brelg  28217  metider  28697  mclsppslem  30221  fundmpss  30407  iunrelexpuztr  36311  frege96d  36341  frege91d  36343  frege98d  36345  frege124d  36353  ssrelrn  39012
  Copyright terms: Public domain W3C validator