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 3929	. 2 ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∈ 𝐴 → ⟨𝐶, 𝐷⟩ ∈ 𝐵))
3		df-br 5096	. 2 ⊢ (𝐶𝐴𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ 𝐴)
4		df-br 5096	. 2 ⊢ (𝐶𝐵𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ 𝐵)
5	2, 3, 4	3imtr4g 296	1 ⊢ (𝜑 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷))

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3898  ⟨cop 4583   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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2808  df-ss 3915  df-br 5096

This theorem is referenced by:  ssbr  5139  sess1  5586  brrelex12  5673  eqbrrdva  5815  predtrss  6276  ersym  8642  ertr  8645  ttrclss  9619  fpwwe2lem5  10535  fpwwe2lem6  10536  fpwwe2lem8  10538  fpwwe2lem11  10541  fpwwe2lem12  10542  fpwwe2  10543  coss12d  14883  fthres2  17845  invfuc  17888  pospo  18253  dirref  18511  efgcpbl  19672  frgpuplem  19688  subrguss  20506  znleval  21495  ustref  24137  ustuqtop4  24162  metider  33930  mclsppslem  35650  fundmpss  35834  eqvrelsym  38724  eqvreltr  38726  iunrelexpuztr  43839  frege96d  43869  frege91d  43871  frege98d  43873  frege124d  43881  grucollcld  44380