Theorem ssbri 5136

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

Syntax hints:   → wi 4   ⊆ wss 3902   class class class wbr 5091

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 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2806  df-ss 3919  df-br 5092

This theorem is referenced by:  brel  5681  swoer  8653  swoord1  8654  swoord2  8655  ecopover  8745  endom  8901  brdom3  10416  brdom5  10417  brdom4  10418  fpwwe2lem12  10530  nqerf  10818  nqerrel  10820  isfull  17816  isfth  17820  fulloppc  17828  fthoppc  17829  fthsect  17831  fthinv  17832  fthmon  17833  fthepi  17834  ffthiso  17835  catcisolem  18014  psss  18483  efgrelex  19661  hlimadd  31168  hhsscms  31253  occllem  31278  nlelchi  32036  hmopidmchi  32126  fundmpss  35799  itg2gt0cn  37714  brresi2  37759  imasubc  49182  imasubc2  49183  fthcomf  49188  uptrlem1  49241  uptrlem3  49243  uptr2  49252  fucoppcfunc  49443  fullthinc2  49482  thincciso  49484  fulltermc2  49543