Theorem ssbri 5130

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

Syntax hints:   → wi 4   ⊆ wss 3889   class class class wbr 5085

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 2811  df-ss 3906  df-br 5086

This theorem is referenced by:  brel  5696  swoer  8675  swoord1  8676  swoord2  8677  ecopover  8768  endom  8926  brdom3  10450  brdom5  10451  brdom4  10452  fpwwe2lem12  10565  nqerf  10853  nqerrel  10855  isfull  17879  isfth  17883  fulloppc  17891  fthoppc  17892  fthsect  17894  fthinv  17895  fthmon  17896  fthepi  17897  ffthiso  17898  catcisolem  18077  psss  18546  efgrelex  19726  hlimadd  31264  hhsscms  31349  occllem  31374  nlelchi  32132  hmopidmchi  32222  fundmpss  35949  itg2gt0cn  37996  brresi2  38041  imasubc  49626  imasubc2  49627  fthcomf  49632  uptrlem1  49685  uptrlem3  49687  uptr2  49696  fucoppcfunc  49887  fullthinc2  49926  thincciso  49928  fulltermc2  49987