Theorem ssbri 5164

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

Syntax hints:   → wi 4   ⊆ wss 3926   class class class wbr 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2809  df-ss 3943  df-br 5120

This theorem is referenced by:  brel  5719  swoer  8750  swoord1  8751  swoord2  8752  ecopover  8835  endom  8993  brdom3  10542  brdom5  10543  brdom4  10544  fpwwe2lem12  10656  nqerf  10944  nqerrel  10946  isfull  17925  isfth  17929  fulloppc  17937  fthoppc  17938  fthsect  17940  fthinv  17941  fthmon  17942  fthepi  17943  ffthiso  17944  catcisolem  18123  psss  18590  efgrelex  19732  hlimadd  31174  hhsscms  31259  occllem  31284  nlelchi  32042  hmopidmchi  32132  fundmpss  35784  itg2gt0cn  37699  brresi2  37744  imasubc  49091  imasubc2  49092  fthcomf  49097  fullthinc2  49337  thincciso  49339  fulltermc2  49397