Theorem ssbrd 5140

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

Syntax hints:   → wi 4   ∈ wcel 2141   ⊆ wss 3902  ⟨cop 4585   class class class wbr 5097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-clel 2836  df-ss 3919  df-br 5098

This theorem is referenced by:  ssbr  5141  sess1  5608  brrelex12  5695  eqbrrdva  5837  predtrss  6303  ersym  8684  ertr  8687  ttrclss  9668  fpwwe2lem5  10586  fpwwe2lem6  10587  fpwwe2lem8  10589  fpwwe2lem11  10592  fpwwe2lem12  10593  fpwwe2  10594  coss12d  14978  fthres2  17957  invfuc  18000  pospo  18365  dirref  18623  efgcpbl  19786  frgpuplem  19802  subrguss  20623  znleval  21593  ustref  24266  ustuqtop4  24291  metider  34151  mclsppslem  35893  fundmpss  36077  eqvrelsym  39148  eqvreltr  39150  iunrelexpuztr  44255  frege96d  44285  frege91d  44287  frege98d  44289  frege124d  44297  grucollcld  44796