Theorem ssbri 5143

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

Syntax hints:   → wi 4   ⊆ wss 3901   class class class wbr 5098

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 2811  df-ss 3918  df-br 5099

This theorem is referenced by:  brel  5689  swoer  8666  swoord1  8667  swoord2  8668  ecopover  8758  endom  8916  brdom3  10438  brdom5  10439  brdom4  10440  fpwwe2lem12  10553  nqerf  10841  nqerrel  10843  isfull  17836  isfth  17840  fulloppc  17848  fthoppc  17849  fthsect  17851  fthinv  17852  fthmon  17853  fthepi  17854  ffthiso  17855  catcisolem  18034  psss  18503  efgrelex  19680  hlimadd  31268  hhsscms  31353  occllem  31378  nlelchi  32136  hmopidmchi  32226  fundmpss  35961  itg2gt0cn  37872  brresi2  37917  imasubc  49392  imasubc2  49393  fthcomf  49398  uptrlem1  49451  uptrlem3  49453  uptr2  49462  fucoppcfunc  49653  fullthinc2  49692  thincciso  49694  fulltermc2  49753