Theorem ssbrd 5186

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3951  ⟨cop 4632   class class class wbr 5143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2816  df-ss 3968  df-br 5144

This theorem is referenced by:  ssbr  5187  sess1  5650  brrelex12  5737  eqbrrdva  5880  predtrss  6343  ersym  8757  ertr  8760  ttrclss  9760  fpwwe2lem5  10675  fpwwe2lem6  10676  fpwwe2lem8  10678  fpwwe2lem11  10681  fpwwe2lem12  10682  fpwwe2  10683  coss12d  15011  fthres2  17979  invfuc  18022  pospo  18390  dirref  18646  efgcpbl  19774  frgpuplem  19790  subrguss  20587  znleval  21573  ustref  24227  ustuqtop4  24253  metider  33893  mclsppslem  35588  fundmpss  35767  eqvrelsym  38606  eqvreltr  38608  iunrelexpuztr  43732  frege96d  43762  frege91d  43764  frege98d  43766  frege124d  43774  grucollcld  44279