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

Theorem ssbrd 4434
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 3456 . 2  |-  ( ph  ->  ( <. C ,  D >.  e.  A  ->  <. C ,  D >.  e.  B ) )
3 df-br 4394 . 2  |-  ( C A D  <->  <. C ,  D >.  e.  A )
4 df-br 4394 . 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 1758    C_ wss 3429   <.cop 3984   class class class wbr 4393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3436  df-ss 3443  df-br 4394
This theorem is referenced by:  ssbri  4435  sess1  4789  brrelex12  4977  coss1  5096  coss2  5097  eqbrrdva  5110  ersym  7216  ertr  7219  fpwwe2lem6  8906  fpwwe2lem7  8907  fpwwe2lem9  8909  fpwwe2lem12  8912  fpwwe2lem13  8913  fpwwe2  8914  fthres2  14953  invfuc  14995  pospo  15254  dirref  15516  efgcpbl  16366  frgpuplem  16382  subrguss  16995  znleval  18105  ustref  19918  ustuqtop4  19944  isucn2  19979  brelg  26085  metider  26459  fundmpss  27714
  Copyright terms: Public domain W3C validator