Theorem ssbrd 5108

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

Syntax hints:   → wi 4   ∈ wcel 2110   ⊆ wss 3935  ⟨cop 4572   class class class wbr 5065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951  df-br 5066

This theorem is referenced by:  ssbr  5109  sess1  5522  brrelex12  5603  eqbrrdva  5739  ersym  8300  ertr  8303  fpwwe2lem6  10056  fpwwe2lem7  10057  fpwwe2lem9  10059  fpwwe2lem12  10062  fpwwe2lem13  10063  fpwwe2  10064  coss12d  14331  fthres2  17201  invfuc  17243  pospo  17582  dirref  17844  efgcpbl  18881  frgpuplem  18897  subrguss  19549  znleval  20700  ustref  22826  ustuqtop4  22852  metider  31134  mclsppslem  32830  fundmpss  33009  eqvrelsym  35839  eqvreltr  35841  iunrelexpuztr  40062  frege96d  40092  frege91d  40094  frege98d  40096  frege124d  40104  grucollcld  40594