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

Theorem ssbrd 5076
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 3917 . 2 (𝜑 → (⟨𝐶, 𝐷⟩ ∈ 𝐴 → ⟨𝐶, 𝐷⟩ ∈ 𝐵))
3 df-br 5034 . 2 (𝐶𝐴𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ 𝐴)
4 df-br 5034 . 2 (𝐶𝐵𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ 𝐵)
52, 3, 43imtr4g 299 1 (𝜑 → (𝐶𝐴𝐷𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  wss 3884  cop 4534   class class class wbr 5033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901  df-br 5034
This theorem is referenced by:  ssbr  5077  sess1  5491  brrelex12  5572  eqbrrdva  5708  ersym  8288  ertr  8291  fpwwe2lem6  10050  fpwwe2lem7  10051  fpwwe2lem9  10053  fpwwe2lem12  10056  fpwwe2lem13  10057  fpwwe2  10058  coss12d  14327  fthres2  17198  invfuc  17240  pospo  17579  dirref  17841  efgcpbl  18878  frgpuplem  18894  subrguss  19547  znleval  20250  ustref  22828  ustuqtop4  22854  metider  31251  mclsppslem  32944  fundmpss  33123  eqvrelsym  35999  eqvreltr  36001  iunrelexpuztr  40417  frege96d  40447  frege91d  40449  frege98d  40451  frege124d  40459  grucollcld  40965
  Copyright terms: Public domain W3C validator