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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ⊆ wss 3895  ⟨cop 4834   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835  df-ss 3896  df-br 5103

This theorem is used by:  ssbr  5148  sess1  5615  brrelex12  5702  eqbrrdva  5846  predtrss  6325  ersym  8734  ertr  8737  ttrclss  9725  fpwwe2lem5  10724  fpwwe2lem6  10725  fpwwe2lem8  10727  fpwwe2lem11  10730  fpwwe2lem12  10731  fpwwe2  10732  coss12d  15131  fthres2  18115  invfuc  18158  pospo  18523  dirref  18781  efgcpbl  19976  frgpuplem  19992  subrguss  20845  znleval  21866  ustref  24544  ustuqtop4  24569  metider  34573  mclsppslem  36435  fundmpss  36625  eqvrelsym  39715  eqvreltr  39717  iunrelexpuztr  44813  frege96d  44843  frege91d  44845  frege98d  44847  frege124d  44855  grucollcld  45338