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

Theorem ssbrd 4626
 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 3567 . 2 (𝜑 → (⟨𝐶, 𝐷⟩ ∈ 𝐴 → ⟨𝐶, 𝐷⟩ ∈ 𝐵))
3 df-br 4584 . 2 (𝐶𝐴𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ 𝐴)
4 df-br 4584 . 2 (𝐶𝐵𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ 𝐵)
52, 3, 43imtr4g 284 1 (𝜑 → (𝐶𝐴𝐷𝐶𝐵𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 1977   ⊆ wss 3540  ⟨cop 4131   class class class wbr 4583 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-br 4584 This theorem is referenced by:  ssbri  4627  sess1  5006  brrelex12  5079  coss1  5199  coss2  5200  eqbrrdva  5213  cnvss  5216  ssrelrn  5237  ersym  7641  ertr  7644  fpwwe2lem6  9336  fpwwe2lem7  9337  fpwwe2lem9  9339  fpwwe2lem12  9342  fpwwe2lem13  9343  fpwwe2  9344  coss12d  13559  fthres2  16415  invfuc  16457  pospo  16796  dirref  17058  efgcpbl  17992  frgpuplem  18008  subrguss  18618  znleval  19722  ustref  21832  ustuqtop4  21858  isucn2  21893  brelg  28801  metider  29265  mclsppslem  30734  fundmpss  30910  iunrelexpuztr  37030  frege96d  37060  frege91d  37062  frege98d  37064  frege124d  37072
 Copyright terms: Public domain W3C validator