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

Theorem ssbrd 4839
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 3735 . 2 (𝜑 → (⟨𝐶, 𝐷⟩ ∈ 𝐴 → ⟨𝐶, 𝐷⟩ ∈ 𝐵))
3 df-br 4797 . 2 (𝐶𝐴𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ 𝐴)
4 df-br 4797 . 2 (𝐶𝐵𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ 𝐵)
52, 3, 43imtr4g 285 1 (𝜑 → (𝐶𝐴𝐷𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2131  wss 3707  cop 4319   class class class wbr 4796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-in 3714  df-ss 3721  df-br 4797
This theorem is referenced by:  ssbr  4840  sess1  5226  brrelex12  5304  eqbrrdva  5439  ersym  7915  ertr  7918  fpwwe2lem6  9641  fpwwe2lem7  9642  fpwwe2lem9  9644  fpwwe2lem12  9647  fpwwe2lem13  9648  fpwwe2  9649  coss12d  13904  fthres2  16785  invfuc  16827  pospo  17166  dirref  17428  efgcpbl  18361  frgpuplem  18377  subrguss  18989  znleval  20097  ustref  22215  ustuqtop4  22241  metider  30238  mclsppslem  31779  fundmpss  31963  iunrelexpuztr  38505  frege96d  38535  frege91d  38537  frege98d  38539  frege124d  38547
  Copyright terms: Public domain W3C validator