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

Theorem ssbrd 4480
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 3488 . 2  |-  ( ph  ->  ( <. C ,  D >.  e.  A  ->  <. C ,  D >.  e.  B ) )
3 df-br 4440 . 2  |-  ( C A D  <->  <. C ,  D >.  e.  A )
4 df-br 4440 . 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 1823    C_ wss 3461   <.cop 4022   class class class wbr 4439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475  df-br 4440
This theorem is referenced by:  ssbri  4481  sess1  4836  brrelex12  5026  coss1  5147  coss2  5148  eqbrrdva  5161  ersym  7315  ertr  7318  fpwwe2lem6  9002  fpwwe2lem7  9003  fpwwe2lem9  9005  fpwwe2lem12  9008  fpwwe2lem13  9009  fpwwe2  9010  coss12d  12890  fthres2  15420  invfuc  15462  pospo  15802  dirref  16064  efgcpbl  16973  frgpuplem  16989  subrguss  17639  znleval  18766  ustref  20887  ustuqtop4  20913  isucn2  20948  brelg  27677  metider  28108  mclsppslem  29207  fundmpss  29437  iunrelexpuztr  38206
  Copyright terms: Public domain W3C validator