Theorem ssbri 5131

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 5130	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷))
3	1, 2	ax-mp 5	1 ⊢ (𝐶𝐴𝐷 → 𝐶𝐵𝐷)

Syntax hints:   → wi 4   ⊆ wss 3890   class class class wbr 5086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812  df-ss 3907  df-br 5087

This theorem is referenced by:  brel  5689  swoer  8668  swoord1  8669  swoord2  8670  ecopover  8761  endom  8919  brdom3  10441  brdom5  10442  brdom4  10443  fpwwe2lem12  10556  nqerf  10844  nqerrel  10846  isfull  17870  isfth  17874  fulloppc  17882  fthoppc  17883  fthsect  17885  fthinv  17886  fthmon  17887  fthepi  17888  ffthiso  17889  catcisolem  18068  psss  18537  efgrelex  19717  hlimadd  31279  hhsscms  31364  occllem  31389  nlelchi  32147  hmopidmchi  32237  fundmpss  35965  itg2gt0cn  38010  brresi2  38055  imasubc  49638  imasubc2  49639  fthcomf  49644  uptrlem1  49697  uptrlem3  49699  uptr2  49708  fucoppcfunc  49899  fullthinc2  49938  thincciso  49940  fulltermc2  49999