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

Theorem ssbrd 4885
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 3795 . 2 (𝜑 → (⟨𝐶, 𝐷⟩ ∈ 𝐴 → ⟨𝐶, 𝐷⟩ ∈ 𝐵))
3 df-br 4843 . 2 (𝐶𝐴𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ 𝐴)
4 df-br 4843 . 2 (𝐶𝐵𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ 𝐵)
52, 3, 43imtr4g 287 1 (𝜑 → (𝐶𝐴𝐷𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2156  wss 3767  cop 4374   class class class wbr 4842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2782
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2791  df-cleq 2797  df-clel 2800  df-in 3774  df-ss 3781  df-br 4843
This theorem is referenced by:  ssbr  4886  sess1  5277  brrelex12  5353  eqbrrdva  5491  ersym  7989  ertr  7992  fpwwe2lem6  9740  fpwwe2lem7  9741  fpwwe2lem9  9743  fpwwe2lem12  9746  fpwwe2lem13  9747  fpwwe2  9748  coss12d  13934  fthres2  16794  invfuc  16836  pospo  17176  dirref  17438  efgcpbl  18368  frgpuplem  18384  subrguss  18997  znleval  20108  ustref  22233  ustuqtop4  22259  metider  30260  mclsppslem  31801  fundmpss  31984  iunrelexpuztr  38509  frege96d  38539  frege91d  38541  frege98d  38543  frege124d  38551
  Copyright terms: Public domain W3C validator