Theorem ssbrd 5155

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

Syntax hints:   → wi 4   ∈ wcel 2143   ⊆ wss 3906  ⟨cop 4596   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 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-clel 2838  df-ss 3923  df-br 5111

This theorem is referenced by:  ssbr  5156  sess1  5628  brrelex12  5715  eqbrrdva  5857  predtrss  6325  ersym  8708  ertr  8711  ttrclss  9690  fpwwe2lem5  10621  fpwwe2lem6  10622  fpwwe2lem8  10624  fpwwe2lem11  10627  fpwwe2lem12  10628  fpwwe2  10629  coss12d  15011  fthres2  17992  invfuc  18035  pospo  18400  dirref  18658  efgcpbl  19827  frgpuplem  19843  subrguss  20673  znleval  21685  ustref  24357  ustuqtop4  24382  metider  34265  mclsppslem  36056  fundmpss  36240  eqvrelsym  39319  eqvreltr  39321  iunrelexpuztr  44428  frege96d  44458  frege91d  44460  frege98d  44462  frege124d  44470  grucollcld  44953