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

Theorem ssbrd 4474
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 3485 . 2  |-  ( ph  ->  ( <. C ,  D >.  e.  A  ->  <. C ,  D >.  e.  B ) )
3 df-br 4434 . 2  |-  ( C A D  <->  <. C ,  D >.  e.  A )
4 df-br 4434 . 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 1802    C_ wss 3458   <.cop 4016   class class class wbr 4433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-in 3465  df-ss 3472  df-br 4434
This theorem is referenced by:  ssbri  4475  sess1  4833  brrelex12  5023  coss1  5144  coss2  5145  eqbrrdva  5158  ersym  7321  ertr  7324  fpwwe2lem6  9011  fpwwe2lem7  9012  fpwwe2lem9  9014  fpwwe2lem12  9017  fpwwe2lem13  9018  fpwwe2  9019  fthres2  15170  invfuc  15212  pospo  15472  dirref  15734  efgcpbl  16643  frgpuplem  16659  subrguss  17312  znleval  18460  ustref  20587  ustuqtop4  20613  isucn2  20648  brelg  27327  metider  27739  mclsppslem  28809  fundmpss  29164  coss12d  37424
  Copyright terms: Public domain W3C validator