Theorem ssbri 5192

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

Syntax hints:   → wi 4   ⊆ wss 3962   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-clel 2813  df-ss 3979  df-br 5148

This theorem is referenced by:  brel  5753  swoer  8774  swoord1  8775  swoord2  8776  ecopover  8859  endom  9017  brdom3  10565  brdom5  10566  brdom4  10567  fpwwe2lem12  10679  nqerf  10967  nqerrel  10969  isfull  17963  isfth  17967  fulloppc  17975  fthoppc  17976  fthsect  17978  fthinv  17979  fthmon  17980  fthepi  17981  ffthiso  17982  catcisolem  18163  psss  18637  efgrelex  19783  hlimadd  31221  hhsscms  31306  occllem  31331  nlelchi  32089  hmopidmchi  32179  fundmpss  35747  itg2gt0cn  37661  brresi2  37706  fullthinc2  48846  thincciso  48848