Theorem ssbri 5152

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

Syntax hints:   → wi 4   ⊆ wss 3914   class class class wbr 5107

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 3931  df-br 5108

This theorem is referenced by:  brel  5703  swoer  8702  swoord1  8703  swoord2  8704  ecopover  8794  endom  8950  brdom3  10481  brdom5  10482  brdom4  10483  fpwwe2lem12  10595  nqerf  10883  nqerrel  10885  isfull  17874  isfth  17878  fulloppc  17886  fthoppc  17887  fthsect  17889  fthinv  17890  fthmon  17891  fthepi  17892  ffthiso  17893  catcisolem  18072  psss  18539  efgrelex  19681  hlimadd  31122  hhsscms  31207  occllem  31232  nlelchi  31990  hmopidmchi  32080  fundmpss  35754  itg2gt0cn  37669  brresi2  37714  imasubc  49140  imasubc2  49141  fthcomf  49146  uptrlem1  49199  uptrlem3  49201  uptr2  49210  fucoppcfunc  49401  fullthinc2  49440  thincciso  49442  fulltermc2  49501