Theorem ssbrd 5111

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3938  ⟨cop 4575   class class class wbr 5068

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-in 3945  df-ss 3954  df-br 5069

This theorem is referenced by:  ssbr  5112  sess1  5525  brrelex12  5606  eqbrrdva  5742  ersym  8303  ertr  8306  fpwwe2lem6  10059  fpwwe2lem7  10060  fpwwe2lem9  10062  fpwwe2lem12  10065  fpwwe2lem13  10066  fpwwe2  10067  coss12d  14334  fthres2  17204  invfuc  17246  pospo  17585  dirref  17847  efgcpbl  18884  frgpuplem  18900  subrguss  19552  znleval  20703  ustref  22829  ustuqtop4  22855  metider  31136  mclsppslem  32832  fundmpss  33011  eqvrelsym  35842  eqvreltr  35844  iunrelexpuztr  40071  frege96d  40101  frege91d  40103  frege98d  40105  frege124d  40113  grucollcld  40603