Theorem ssbrd 5190

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

Syntax hints:   → wi 4   ∈ wcel 2105   ⊆ wss 3962  ⟨cop 4636   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-clel 2813  df-ss 3979  df-br 5148

This theorem is referenced by:  ssbr  5191  sess1  5653  brrelex12  5740  eqbrrdva  5882  predtrss  6344  ersym  8755  ertr  8758  ttrclss  9757  fpwwe2lem5  10672  fpwwe2lem6  10673  fpwwe2lem8  10675  fpwwe2lem11  10678  fpwwe2lem12  10679  fpwwe2  10680  coss12d  15007  fthres2  17985  invfuc  18030  pospo  18402  dirref  18658  efgcpbl  19788  frgpuplem  19804  subrguss  20603  znleval  21590  ustref  24242  ustuqtop4  24268  metider  33854  mclsppslem  35567  fundmpss  35747  eqvrelsym  38586  eqvreltr  38588  iunrelexpuztr  43708  frege96d  43738  frege91d  43740  frege98d  43742  frege124d  43750  grucollcld  44255