Theorem ssbri 5157

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

Syntax hints:   → wi 4   ⊆ wss 3906   class class class wbr 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-clel 2838  df-ss 3923  df-br 5111

This theorem is referenced by:  brel  5728  swoer  8727  swoord1  8728  swoord2  8729  ecopover  8820  endom  8977  brdom3  10513  brdom5  10514  brdom4  10515  fpwwe2lem12  10628  nqerf  10916  nqerrel  10918  isfull  17970  isfth  17974  fulloppc  17982  fthoppc  17983  fthsect  17985  fthinv  17986  fthmon  17987  fthepi  17988  ffthiso  17989  catcisolem  18168  psss  18637  efgrelex  19822  hlimadd  31523  hhsscms  31608  occllem  31633  nlelchi  32391  hmopidmchi  32481  fundmpss  36237  itg2gt0cn  38304  brresi2  38349  imasubc  49906  imasubc2  49907  fthcomf  49912  uptrlem1  49965  uptrlem3  49967  uptr2  49976  fucoppcfunc  50167  fullthinc2  50206  thincciso  50208  fulltermc2  50267