Theorem ssbrd 5143

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3903  ⟨cop 4588   class class class wbr 5100

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 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812  df-ss 3920  df-br 5101

This theorem is referenced by:  ssbr  5144  sess1  5597  brrelex12  5684  eqbrrdva  5826  predtrss  6288  ersym  8658  ertr  8661  ttrclss  9641  fpwwe2lem5  10558  fpwwe2lem6  10559  fpwwe2lem8  10561  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  coss12d  14907  fthres2  17870  invfuc  17913  pospo  18278  dirref  18536  efgcpbl  19697  frgpuplem  19713  subrguss  20532  znleval  21521  ustref  24175  ustuqtop4  24200  metider  34071  mclsppslem  35796  fundmpss  35980  eqvrelsym  38937  eqvreltr  38939  iunrelexpuztr  44072  frege96d  44102  frege91d  44104  frege98d  44106  frege124d  44114  grucollcld  44613