Theorem ssbrd 5138

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

Step	Hyp	Ref	Expression
1		ssbrd.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2	1	sseld 3936	. 2 ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∈ 𝐴 → ⟨𝐶, 𝐷⟩ ∈ 𝐵))
3		df-br 5096	. 2 ⊢ (𝐶𝐴𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ 𝐴)
4		df-br 5096	. 2 ⊢ (𝐶𝐵𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ 𝐵)
5	2, 3, 4	3imtr4g 296	1 ⊢ (𝜑 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷))

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3905  ⟨cop 4585   class class class wbr 5095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803  df-ss 3922  df-br 5096

This theorem is referenced by:  ssbr  5139  sess1  5588  brrelex12  5675  eqbrrdva  5816  predtrss  6274  ersym  8644  ertr  8647  ttrclss  9635  fpwwe2lem5  10548  fpwwe2lem6  10549  fpwwe2lem8  10551  fpwwe2lem11  10554  fpwwe2lem12  10555  fpwwe2  10556  coss12d  14897  fthres2  17859  invfuc  17902  pospo  18267  dirref  18525  efgcpbl  19653  frgpuplem  19669  subrguss  20490  znleval  21479  ustref  24122  ustuqtop4  24148  metider  33863  mclsppslem  35558  fundmpss  35742  eqvrelsym  38584  eqvreltr  38586  iunrelexpuztr  43695  frege96d  43725  frege91d  43727  frege98d  43729  frege124d  43737  grucollcld  44236