Theorem ssbrd 5153

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3917  ⟨cop 4598   class class class wbr 5110

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 2804  df-ss 3934  df-br 5111

This theorem is referenced by:  ssbr  5154  sess1  5606  brrelex12  5693  eqbrrdva  5836  predtrss  6298  ersym  8686  ertr  8689  ttrclss  9680  fpwwe2lem5  10595  fpwwe2lem6  10596  fpwwe2lem8  10598  fpwwe2lem11  10601  fpwwe2lem12  10602  fpwwe2  10603  coss12d  14945  fthres2  17903  invfuc  17946  pospo  18311  dirref  18567  efgcpbl  19693  frgpuplem  19709  subrguss  20503  znleval  21471  ustref  24113  ustuqtop4  24139  metider  33891  mclsppslem  35577  fundmpss  35761  eqvrelsym  38603  eqvreltr  38605  iunrelexpuztr  43715  frege96d  43745  frege91d  43747  frege98d  43749  frege124d  43757  grucollcld  44256