Theorem ssbri 5150

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

Syntax hints:   → wi 4   ⊆ wss 3907   class class class wbr 5105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-clel 2840  df-ss 3924  df-br 5106

This theorem is referenced by:  brel  5717  swoer  8714  swoord1  8715  swoord2  8716  ecopover  8807  endom  8964  brdom3  10500  brdom5  10501  brdom4  10502  fpwwe2lem12  10615  nqerf  10903  nqerrel  10905  isfull  17959  isfth  17963  fulloppc  17971  fthoppc  17972  fthsect  17974  fthinv  17975  fthmon  17976  fthepi  17977  ffthiso  17978  catcisolem  18157  psss  18626  efgrelex  19812  hlimadd  31454  hhsscms  31539  occllem  31564  nlelchi  32322  hmopidmchi  32412  fundmpss  36130  itg2gt0cn  38186  brresi2  38231  imasubc  49780  imasubc2  49781  fthcomf  49786  uptrlem1  49839  uptrlem3  49841  uptr2  49850  fucoppcfunc  50041  fullthinc2  50080  thincciso  50082  fulltermc2  50141