Theorem ssbrd 5147

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

Syntax hints:   → wi 4   ∈ wcel 2145   ⊆ wss 3907  ⟨cop 4591   class class class wbr 5104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-clel 2840  df-ss 3924  df-br 5105

This theorem is referenced by:  ssbr  5148  sess1  5616  brrelex12  5703  eqbrrdva  5845  predtrss  6312  ersym  8695  ertr  8698  ttrclss  9677  fpwwe2lem5  10608  fpwwe2lem6  10609  fpwwe2lem8  10611  fpwwe2lem11  10614  fpwwe2lem12  10615  fpwwe2  10616  coss12d  14997  fthres2  17979  invfuc  18022  pospo  18387  dirref  18645  efgcpbl  19814  frgpuplem  19830  subrguss  20660  znleval  21661  ustref  24333  ustuqtop4  24358  metider  34196  mclsppslem  35941  fundmpss  36125  eqvrelsym  39195  eqvreltr  39197  iunrelexpuztr  44302  frege96d  44332  frege91d  44334  frege98d  44336  frege124d  44344  grucollcld  44829