Theorem ssbrd 5128

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3889  ⟨cop 4573   class class class wbr 5085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2811  df-ss 3906  df-br 5086

This theorem is referenced by:  ssbr  5129  sess1  5596  brrelex12  5683  eqbrrdva  5824  predtrss  6286  ersym  8656  ertr  8659  ttrclss  9641  fpwwe2lem5  10558  fpwwe2lem6  10559  fpwwe2lem8  10561  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  coss12d  14934  fthres2  17901  invfuc  17944  pospo  18309  dirref  18567  efgcpbl  19731  frgpuplem  19747  subrguss  20564  znleval  21534  ustref  24184  ustuqtop4  24209  metider  34038  mclsppslem  35765  fundmpss  35949  eqvrelsym  39010  eqvreltr  39012  iunrelexpuztr  44146  frege96d  44176  frege91d  44178  frege98d  44180  frege124d  44188  grucollcld  44687