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

Theorem ssbrd 4661
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 3586 . 2 (𝜑 → (⟨𝐶, 𝐷⟩ ∈ 𝐴 → ⟨𝐶, 𝐷⟩ ∈ 𝐵))
3 df-br 4619 . 2 (𝐶𝐴𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ 𝐴)
4 df-br 4619 . 2 (𝐶𝐵𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ 𝐵)
52, 3, 43imtr4g 285 1 (𝜑 → (𝐶𝐴𝐷𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  wss 3559  cop 4159   class class class wbr 4618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3566  df-ss 3573  df-br 4619
This theorem is referenced by:  ssbri  4662  sess1  5047  brrelex12  5120  coss1  5242  coss2  5243  eqbrrdva  5256  cnvss  5259  ssrelrn  5280  ersym  7706  ertr  7709  fpwwe2lem6  9409  fpwwe2lem7  9410  fpwwe2lem9  9412  fpwwe2lem12  9415  fpwwe2lem13  9416  fpwwe2  9417  coss12d  13653  fthres2  16524  invfuc  16566  pospo  16905  dirref  17167  efgcpbl  18101  frgpuplem  18117  subrguss  18727  znleval  19835  ustref  21945  ustuqtop4  21971  isucn2  22006  brelg  29287  metider  29743  mclsppslem  31223  fundmpss  31403  iunrelexpuztr  37527  frege96d  37557  frege91d  37559  frege98d  37561  frege124d  37569
  Copyright terms: Public domain W3C validator