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

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3913  ⟨cop 4597   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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-br 5111

This theorem is referenced by:  ssbr  5154  sess1  5606  brrelex12  5689  eqbrrdva  5830  predtrss  6281  ersym  8667  ertr  8670  ttrclss  9665  fpwwe2lem5  10580  fpwwe2lem6  10581  fpwwe2lem8  10583  fpwwe2lem11  10586  fpwwe2lem12  10587  fpwwe2  10588  coss12d  14869  fthres2  17833  invfuc  17877  pospo  18248  dirref  18504  efgcpbl  19552  frgpuplem  19568  subrguss  20285  znleval  20998  ustref  23607  ustuqtop4  23633  metider  32564  mclsppslem  34264  fundmpss  34427  eqvrelsym  37140  eqvreltr  37142  iunrelexpuztr  42113  frege96d  42143  frege91d  42145  frege98d  42147  frege124d  42155  grucollcld  42662