Theorem ssbrd 5150

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3914  ⟨cop 4595   class class class wbr 5107

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 3931  df-br 5108

This theorem is referenced by:  ssbr  5151  sess1  5603  brrelex12  5690  eqbrrdva  5833  predtrss  6295  ersym  8683  ertr  8686  ttrclss  9673  fpwwe2lem5  10588  fpwwe2lem6  10589  fpwwe2lem8  10591  fpwwe2lem11  10594  fpwwe2lem12  10595  fpwwe2  10596  coss12d  14938  fthres2  17896  invfuc  17939  pospo  18304  dirref  18560  efgcpbl  19686  frgpuplem  19702  subrguss  20496  znleval  21464  ustref  24106  ustuqtop4  24132  metider  33884  mclsppslem  35570  fundmpss  35754  eqvrelsym  38596  eqvreltr  38598  iunrelexpuztr  43708  frege96d  43738  frege91d  43740  frege98d  43742  frege124d  43750  grucollcld  44249