Theorem ssbri 5188

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

Syntax hints:   → wi 4   ⊆ wss 3951   class class class wbr 5143

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 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2816  df-ss 3968  df-br 5144

This theorem is referenced by:  brel  5750  swoer  8776  swoord1  8777  swoord2  8778  ecopover  8861  endom  9019  brdom3  10568  brdom5  10569  brdom4  10570  fpwwe2lem12  10682  nqerf  10970  nqerrel  10972  isfull  17957  isfth  17961  fulloppc  17969  fthoppc  17970  fthsect  17972  fthinv  17973  fthmon  17974  fthepi  17975  ffthiso  17976  catcisolem  18155  psss  18625  efgrelex  19769  hlimadd  31212  hhsscms  31297  occllem  31322  nlelchi  32080  hmopidmchi  32170  fundmpss  35767  itg2gt0cn  37682  brresi2  37727  fullthinc2  49100  thincciso  49102