Theorem ssbri 5140

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

Syntax hints:   → wi 4   ⊆ wss 3905   class class class wbr 5095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803  df-ss 3922  df-br 5096

This theorem is referenced by:  brel  5688  swoer  8663  swoord1  8664  swoord2  8665  ecopover  8755  endom  8911  brdom3  10441  brdom5  10442  brdom4  10443  fpwwe2lem12  10555  nqerf  10843  nqerrel  10845  isfull  17837  isfth  17841  fulloppc  17849  fthoppc  17850  fthsect  17852  fthinv  17853  fthmon  17854  fthepi  17855  ffthiso  17856  catcisolem  18035  psss  18504  efgrelex  19648  hlimadd  31155  hhsscms  31240  occllem  31265  nlelchi  32023  hmopidmchi  32113  fundmpss  35739  itg2gt0cn  37654  brresi2  37699  imasubc  49137  imasubc2  49138  fthcomf  49143  uptrlem1  49196  uptrlem3  49198  uptr2  49207  fucoppcfunc  49398  fullthinc2  49437  thincciso  49439  fulltermc2  49498