Theorem ssbrd 5082

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

Syntax hints:   → wi 4   ∈ wcel 2112   ⊆ wss 3853  ⟨cop 4533   class class class wbr 5039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870  df-br 5040

This theorem is referenced by:  ssbr  5083  sess1  5504  brrelex12  5586  eqbrrdva  5723  ersym  8381  ertr  8384  fpwwe2lem5  10214  fpwwe2lem6  10215  fpwwe2lem8  10217  fpwwe2lem11  10220  fpwwe2lem12  10221  fpwwe2  10222  coss12d  14500  fthres2  17393  invfuc  17437  pospo  17805  dirref  18061  efgcpbl  19100  frgpuplem  19116  subrguss  19769  znleval  20473  ustref  23070  ustuqtop4  23096  metider  31512  mclsppslem  33212  fundmpss  33410  eqvrelsym  36404  eqvreltr  36406  iunrelexpuztr  40945  frege96d  40975  frege91d  40977  frege98d  40979  frege124d  40987  grucollcld  41492