Theorem ssbri 5134

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

Syntax hints:   → wi 4   ⊆ wss 3900   class class class wbr 5089

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 2112

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2804  df-ss 3917  df-br 5090

This theorem is referenced by:  brel  5679  swoer  8648  swoord1  8649  swoord2  8650  ecopover  8740  endom  8896  brdom3  10411  brdom5  10412  brdom4  10413  fpwwe2lem12  10525  nqerf  10813  nqerrel  10815  isfull  17811  isfth  17815  fulloppc  17823  fthoppc  17824  fthsect  17826  fthinv  17827  fthmon  17828  fthepi  17829  ffthiso  17830  catcisolem  18009  psss  18478  efgrelex  19656  hlimadd  31163  hhsscms  31248  occllem  31273  nlelchi  32031  hmopidmchi  32121  fundmpss  35779  itg2gt0cn  37694  brresi2  37739  imasubc  49162  imasubc2  49163  fthcomf  49168  uptrlem1  49221  uptrlem3  49223  uptr2  49232  fucoppcfunc  49423  fullthinc2  49462  thincciso  49464  fulltermc2  49523