Theorem ssbri 5145

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

Syntax hints:   → wi 4   ⊆ wss 3903   class class class wbr 5100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812  df-ss 3920  df-br 5101

This theorem is referenced by:  brel  5697  swoer  8677  swoord1  8678  swoord2  8679  ecopover  8770  endom  8928  brdom3  10450  brdom5  10451  brdom4  10452  fpwwe2lem12  10565  nqerf  10853  nqerrel  10855  isfull  17848  isfth  17852  fulloppc  17860  fthoppc  17861  fthsect  17863  fthinv  17864  fthmon  17865  fthepi  17866  ffthiso  17867  catcisolem  18046  psss  18515  efgrelex  19692  hlimadd  31280  hhsscms  31365  occllem  31390  nlelchi  32148  hmopidmchi  32238  fundmpss  35980  itg2gt0cn  37920  brresi2  37965  imasubc  49504  imasubc2  49505  fthcomf  49510  uptrlem1  49563  uptrlem3  49565  uptr2  49574  fucoppcfunc  49765  fullthinc2  49804  thincciso  49806  fulltermc2  49865