Theorem ssbrd 5209

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3976  ⟨cop 4654   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clel 2819  df-ss 3993  df-br 5167

This theorem is referenced by:  ssbr  5210  sess1  5665  brrelex12  5752  eqbrrdva  5894  predtrss  6354  ersym  8775  ertr  8778  ttrclss  9789  fpwwe2lem5  10704  fpwwe2lem6  10705  fpwwe2lem8  10707  fpwwe2lem11  10710  fpwwe2lem12  10711  fpwwe2  10712  coss12d  15021  fthres2  17999  invfuc  18044  pospo  18415  dirref  18671  efgcpbl  19798  frgpuplem  19814  subrguss  20615  znleval  21596  ustref  24248  ustuqtop4  24274  metider  33840  mclsppslem  35551  fundmpss  35730  eqvrelsym  38561  eqvreltr  38563  iunrelexpuztr  43681  frege96d  43711  frege91d  43713  frege98d  43715  frege124d  43723  grucollcld  44229