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

Theorem ssbrd 5186
Description: Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.)
Hypothesis
Ref Expression
ssbrd.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
ssbrd (𝜑 → (𝐶𝐴𝐷𝐶𝐵𝐷))

Proof of Theorem ssbrd
StepHypRef Expression
1 ssbrd.1 . . 3 (𝜑𝐴𝐵)
21sseld 3982 . 2 (𝜑 → (⟨𝐶, 𝐷⟩ ∈ 𝐴 → ⟨𝐶, 𝐷⟩ ∈ 𝐵))
3 df-br 5144 . 2 (𝐶𝐴𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ 𝐴)
4 df-br 5144 . 2 (𝐶𝐵𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ 𝐵)
52, 3, 43imtr4g 296 1 (𝜑 → (𝐶𝐴𝐷𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  wss 3951  cop 4632   class class class wbr 5143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2816  df-ss 3968  df-br 5144
This theorem is referenced by:  ssbr  5187  sess1  5650  brrelex12  5737  eqbrrdva  5880  predtrss  6343  ersym  8757  ertr  8760  ttrclss  9760  fpwwe2lem5  10675  fpwwe2lem6  10676  fpwwe2lem8  10678  fpwwe2lem11  10681  fpwwe2lem12  10682  fpwwe2  10683  coss12d  15011  fthres2  17979  invfuc  18022  pospo  18390  dirref  18646  efgcpbl  19774  frgpuplem  19790  subrguss  20587  znleval  21573  ustref  24227  ustuqtop4  24253  metider  33893  mclsppslem  35588  fundmpss  35767  eqvrelsym  38606  eqvreltr  38608  iunrelexpuztr  43732  frege96d  43762  frege91d  43764  frege98d  43766  frege124d  43774  grucollcld  44279
  Copyright terms: Public domain W3C validator