Theorem ssbrd 5117

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

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3887  ⟨cop 4567   class class class wbr 5074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-br 5075

This theorem is referenced by:  ssbr  5118  sess1  5557  brrelex12  5639  eqbrrdva  5778  predtrss  6225  ersym  8510  ertr  8513  ttrclss  9478  fpwwe2lem5  10391  fpwwe2lem6  10392  fpwwe2lem8  10394  fpwwe2lem11  10397  fpwwe2lem12  10398  fpwwe2  10399  coss12d  14683  fthres2  17648  invfuc  17692  pospo  18063  dirref  18319  efgcpbl  19362  frgpuplem  19378  subrguss  20039  znleval  20762  ustref  23370  ustuqtop4  23396  metider  31844  mclsppslem  33545  fundmpss  33740  eqvrelsym  36718  eqvreltr  36720  iunrelexpuztr  41327  frege96d  41357  frege91d  41359  frege98d  41361  frege124d  41369  grucollcld  41878