Theorem ssbrd 5141

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3901  ⟨cop 4586   class class class wbr 5098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2811  df-ss 3918  df-br 5099

This theorem is referenced by:  ssbr  5142  sess1  5589  brrelex12  5676  eqbrrdva  5818  predtrss  6280  ersym  8647  ertr  8650  ttrclss  9629  fpwwe2lem5  10546  fpwwe2lem6  10547  fpwwe2lem8  10549  fpwwe2lem11  10552  fpwwe2lem12  10553  fpwwe2  10554  coss12d  14895  fthres2  17858  invfuc  17901  pospo  18266  dirref  18524  efgcpbl  19685  frgpuplem  19701  subrguss  20520  znleval  21509  ustref  24163  ustuqtop4  24188  metider  34051  mclsppslem  35777  fundmpss  35961  eqvrelsym  38862  eqvreltr  38864  iunrelexpuztr  43960  frege96d  43990  frege91d  43992  frege98d  43994  frege124d  44002  grucollcld  44501