Theorem ssbrd 5122

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

Syntax hints:   → wi 4   ∈ wcel 2119   ⊆ wss 3890  ⟨cop 4568   class class class wbr 5079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clel 2815  df-ss 3907  df-br 5080

This theorem is referenced by:  ssbr  5123  sess1  5590  brrelex12  5677  eqbrrdva  5818  predtrss  6280  ersym  8653  ertr  8656  ttrclss  9639  fpwwe2lem5  10556  fpwwe2lem6  10557  fpwwe2lem8  10559  fpwwe2lem11  10562  fpwwe2lem12  10563  fpwwe2  10564  coss12d  14932  fthres2  17899  invfuc  17942  pospo  18307  dirref  18565  efgcpbl  19729  frgpuplem  19745  subrguss  20566  znleval  21536  ustref  24209  ustuqtop4  24234  metider  34085  mclsppslem  35818  fundmpss  36002  eqvrelsym  39063  eqvreltr  39065  iunrelexpuztr  44170  frege96d  44200  frege91d  44202  frege98d  44204  frege124d  44212  grucollcld  44711