Theorem ssbri 5194

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

Syntax hints:   → wi 4   ⊆ wss 3944   class class class wbr 5149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-clel 2802  df-ss 3961  df-br 5150

This theorem is referenced by:  brel  5743  swoer  8755  swoord1  8756  swoord2  8757  ecopover  8840  endom  9000  brdom3  10553  brdom5  10554  brdom4  10555  fpwwe2lem12  10667  nqerf  10955  nqerrel  10957  isfull  17902  isfth  17906  fulloppc  17914  fthoppc  17915  fthsect  17917  fthinv  17918  fthmon  17919  fthepi  17920  ffthiso  17921  catcisolem  18102  psss  18575  efgrelex  19718  hlimadd  31075  hhsscms  31160  occllem  31185  nlelchi  31943  hmopidmchi  32033  fundmpss  35493  itg2gt0cn  37279  brresi2  37324  fullthinc2  48239  thincciso  48241