Theorem ssbrd 5152

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3902  ⟨cop 4593   class class class wbr 5107

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 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2837  df-ss 3919  df-br 5108

This theorem is used by:  ssbr  5153  sess1  5624  brrelex12  5711  eqbrrdva  5853  predtrss  6324  ersym  8713  ertr  8716  ttrclss  9703  fpwwe2lem5  10648  fpwwe2lem6  10649  fpwwe2lem8  10651  fpwwe2lem11  10654  fpwwe2lem12  10655  fpwwe2  10656  coss12d  15049  fthres2  18029  invfuc  18072  pospo  18437  dirref  18695  efgcpbl  19889  frgpuplem  19905  subrguss  20755  znleval  21773  ustref  24451  ustuqtop4  24476  metider  34412  mclsppslem  36170  fundmpss  36354  eqvrelsym  39445  eqvreltr  39447  iunrelexpuztr  44567  frege96d  44597  frege91d  44599  frege98d  44601  frege124d  44609  grucollcld  45092