Theorem ssbrd 4972

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

Syntax hints:   → wi 4   ∈ wcel 2050   ⊆ wss 3830  ⟨cop 4447   class class class wbr 4929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2751

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2760  df-cleq 2772  df-clel 2847  df-in 3837  df-ss 3844  df-br 4930

This theorem is referenced by:  ssbr  4973  sess1  5375  brrelex12  5454  eqbrrdva  5590  ersym  8101  ertr  8104  fpwwe2lem6  9855  fpwwe2lem7  9856  fpwwe2lem9  9858  fpwwe2lem12  9861  fpwwe2lem13  9862  fpwwe2  9863  coss12d  14193  fthres2  17060  invfuc  17102  pospo  17441  dirref  17703  efgcpbl  18642  frgpuplem  18658  subrguss  19273  znleval  20403  ustref  22530  ustuqtop4  22556  metider  30775  mclsppslem  32347  fundmpss  32526  eqvrelsym  35282  eqvreltr  35284  iunrelexpuztr  39424  frege96d  39454  frege91d  39456  frege98d  39458  frege124d  39466  grucollcld  39968