Theorem ssbrd 5113

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3883  ⟨cop 4564   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-br 5071

This theorem is referenced by:  ssbr  5114  sess1  5548  brrelex12  5630  eqbrrdva  5767  predtrss  6214  ersym  8468  ertr  8471  fpwwe2lem5  10322  fpwwe2lem6  10323  fpwwe2lem8  10325  fpwwe2lem11  10328  fpwwe2lem12  10329  fpwwe2  10330  coss12d  14611  fthres2  17564  invfuc  17608  pospo  17978  dirref  18234  efgcpbl  19277  frgpuplem  19293  subrguss  19954  znleval  20674  ustref  23278  ustuqtop4  23304  metider  31746  mclsppslem  33445  fundmpss  33646  ttrclss  33706  eqvrelsym  36645  eqvreltr  36647  iunrelexpuztr  41216  frege96d  41246  frege91d  41248  frege98d  41250  frege124d  41258  grucollcld  41767