Theorem ssbrd 5148

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899  ⟨cop 4590   class class class wbr 5103

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 2835  df-ss 3916  df-br 5104

This theorem is used by:  ssbr  5149  sess1  5620  brrelex12  5707  eqbrrdva  5849  predtrss  6320  ersym  8709  ertr  8712  ttrclss  9699  fpwwe2lem5  10644  fpwwe2lem6  10645  fpwwe2lem8  10647  fpwwe2lem11  10650  fpwwe2lem12  10651  fpwwe2  10652  coss12d  15045  fthres2  18023  invfuc  18066  pospo  18431  dirref  18689  efgcpbl  19883  frgpuplem  19899  subrguss  20749  znleval  21767  ustref  24445  ustuqtop4  24470  metider  34404  mclsppslem  36162  fundmpss  36346  eqvrelsym  39437  eqvreltr  39439  iunrelexpuztr  44559  frege96d  44589  frege91d  44591  frege98d  44593  frege124d  44601  grucollcld  45084