Theorem ssbrd 5162

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3926  ⟨cop 4607   class class class wbr 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2809  df-ss 3943  df-br 5120

This theorem is referenced by:  ssbr  5163  sess1  5619  brrelex12  5706  eqbrrdva  5849  predtrss  6311  ersym  8731  ertr  8734  ttrclss  9734  fpwwe2lem5  10649  fpwwe2lem6  10650  fpwwe2lem8  10652  fpwwe2lem11  10655  fpwwe2lem12  10656  fpwwe2  10657  coss12d  14991  fthres2  17947  invfuc  17990  pospo  18355  dirref  18611  efgcpbl  19737  frgpuplem  19753  subrguss  20547  znleval  21515  ustref  24157  ustuqtop4  24183  metider  33925  mclsppslem  35605  fundmpss  35784  eqvrelsym  38623  eqvreltr  38625  iunrelexpuztr  43743  frege96d  43773  frege91d  43775  frege98d  43777  frege124d  43785  grucollcld  44284