Theorem ssbrd 5139

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

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3901  ⟨cop 4583   class class class wbr 5096

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3444  df-in 3908  df-ss 3918  df-br 5097

This theorem is referenced by:  ssbr  5140  sess1  5592  brrelex12  5674  eqbrrdva  5815  predtrss  6265  ersym  8585  ertr  8588  ttrclss  9581  fpwwe2lem5  10496  fpwwe2lem6  10497  fpwwe2lem8  10499  fpwwe2lem11  10502  fpwwe2lem12  10503  fpwwe2  10504  coss12d  14782  fthres2  17745  invfuc  17789  pospo  18160  dirref  18416  efgcpbl  19457  frgpuplem  19473  subrguss  20143  znleval  20867  ustref  23475  ustuqtop4  23501  metider  32140  mclsppslem  33842  fundmpss  34024  eqvrelsym  36923  eqvreltr  36925  iunrelexpuztr  41700  frege96d  41730  frege91d  41732  frege98d  41734  frege124d  41742  grucollcld  42251