Theorem ssbrd 5134

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

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3902  ⟨cop 4582   class class class wbr 5091

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 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2806  df-ss 3919  df-br 5092

This theorem is referenced by:  ssbr  5135  sess1  5581  brrelex12  5668  eqbrrdva  5809  predtrss  6269  ersym  8634  ertr  8637  ttrclss  9610  fpwwe2lem5  10526  fpwwe2lem6  10527  fpwwe2lem8  10529  fpwwe2lem11  10532  fpwwe2lem12  10533  fpwwe2  10534  coss12d  14879  fthres2  17841  invfuc  17884  pospo  18249  dirref  18507  efgcpbl  19669  frgpuplem  19685  subrguss  20503  znleval  21492  ustref  24135  ustuqtop4  24160  metider  33905  mclsppslem  35625  fundmpss  35809  eqvrelsym  38648  eqvreltr  38650  iunrelexpuztr  43758  frege96d  43788  frege91d  43790  frege98d  43792  frege124d  43800  grucollcld  44299