Theorem ssbrd 4839

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

Syntax hints:   → wi 4   ∈ wcel 2131   ⊆ wss 3707  ⟨cop 4319   class class class wbr 4796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-in 3714  df-ss 3721  df-br 4797

This theorem is referenced by:  ssbr  4840  sess1  5226  brrelex12  5304  eqbrrdva  5439  ersym  7915  ertr  7918  fpwwe2lem6  9641  fpwwe2lem7  9642  fpwwe2lem9  9644  fpwwe2lem12  9647  fpwwe2lem13  9648  fpwwe2  9649  coss12d  13904  fthres2  16785  invfuc  16827  pospo  17166  dirref  17428  efgcpbl  18361  frgpuplem  18377  subrguss  18989  znleval  20097  ustref  22215  ustuqtop4  22241  metider  30238  mclsppslem  31779  fundmpss  31963  iunrelexpuztr  38505  frege96d  38535  frege91d  38537  frege98d  38539  frege124d  38547