Theorem ssbri 5138

Description: Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.)

Hypothesis

Ref	Expression
ssbri.1	⊢ 𝐴 ⊆ 𝐵

Assertion

Ref	Expression
ssbri	⊢ (𝐶𝐴𝐷 → 𝐶𝐵𝐷)

Proof of Theorem ssbri

Step	Hyp	Ref	Expression
1		ssbri.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		ssbr 5137	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷))
3	1, 2	ax-mp 5	1 ⊢ (𝐶𝐴𝐷 → 𝐶𝐵𝐷)

Syntax hints:   → wi 4   ⊆ wss 3898   class class class wbr 5093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2808  df-ss 3915  df-br 5094

This theorem is referenced by:  brel  5684  swoer  8659  swoord1  8660  swoord2  8661  ecopover  8751  endom  8908  brdom3  10426  brdom5  10427  brdom4  10428  fpwwe2lem12  10540  nqerf  10828  nqerrel  10830  isfull  17821  isfth  17825  fulloppc  17833  fthoppc  17834  fthsect  17836  fthinv  17837  fthmon  17838  fthepi  17839  ffthiso  17840  catcisolem  18019  psss  18488  efgrelex  19665  hlimadd  31175  hhsscms  31260  occllem  31285  nlelchi  32043  hmopidmchi  32133  fundmpss  35832  itg2gt0cn  37735  brresi2  37780  imasubc  49276  imasubc2  49277  fthcomf  49282  uptrlem1  49335  uptrlem3  49337  uptr2  49346  fucoppcfunc  49537  fullthinc2  49576  thincciso  49578  fulltermc2  49637