Theorem ssbrd 5156

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ⊆ wss 3906  ⟨cop 4597   class class class wbr 5111

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2840  df-ss 3923  df-br 5112

This theorem is used by:  ssbr  5157  sess1  5628  brrelex12  5715  eqbrrdva  5857  predtrss  6327  ersym  8709  ertr  8712  ttrclss  9692  fpwwe2lem5  10631  fpwwe2lem6  10632  fpwwe2lem8  10634  fpwwe2lem11  10637  fpwwe2lem12  10638  fpwwe2  10639  coss12d  15028  fthres2  18008  invfuc  18051  pospo  18416  dirref  18674  efgcpbl  19849  frgpuplem  19865  subrguss  20715  znleval  21733  ustref  24405  ustuqtop4  24430  metider  34307  mclsppslem  36088  fundmpss  36272  eqvrelsym  39371  eqvreltr  39373  iunrelexpuztr  44478  frege96d  44508  frege91d  44510  frege98d  44512  frege124d  44520  grucollcld  45003