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

Theorem ssbrd 4481
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 3496 . 2  |-  ( ph  ->  ( <. C ,  D >.  e.  A  ->  <. C ,  D >.  e.  B ) )
3 df-br 4441 . 2  |-  ( C A D  <->  <. C ,  D >.  e.  A )
4 df-br 4441 . 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 1762    C_ wss 3469   <.cop 4026   class class class wbr 4440
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-in 3476  df-ss 3483  df-br 4441
This theorem is referenced by:  ssbri  4482  sess1  4840  brrelex12  5029  coss1  5149  coss2  5150  eqbrrdva  5163  ersym  7313  ertr  7316  fpwwe2lem6  9002  fpwwe2lem7  9003  fpwwe2lem9  9005  fpwwe2lem12  9008  fpwwe2lem13  9009  fpwwe2  9010  fthres2  15148  invfuc  15190  pospo  15449  dirref  15711  efgcpbl  16563  frgpuplem  16579  subrguss  17220  znleval  18353  ustref  20449  ustuqtop4  20475  isucn2  20510  brelg  26985  metider  27359  fundmpss  28623  coss12d  36654
  Copyright terms: Public domain W3C validator