Theorem ssbri 5144

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

Syntax hints:   → wi 4   ⊆ wss 3904   class class class wbr 5099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-clel 2836  df-ss 3921  df-br 5100

This theorem is referenced by:  brel  5710  swoer  8705  swoord1  8706  swoord2  8707  ecopover  8798  endom  8956  brdom3  10482  brdom5  10483  brdom4  10484  fpwwe2lem12  10597  nqerf  10885  nqerrel  10887  isfull  17928  isfth  17932  fulloppc  17940  fthoppc  17941  fthsect  17943  fthinv  17944  fthmon  17945  fthepi  17946  ffthiso  17947  catcisolem  18126  psss  18595  efgrelex  19774  hlimadd  31342  hhsscms  31427  occllem  31452  nlelchi  32210  hmopidmchi  32300  fundmpss  36081  itg2gt0cn  38138  brresi2  38183  imasubc  49736  imasubc2  49737  fthcomf  49742  uptrlem1  49795  uptrlem3  49797  uptr2  49806  fucoppcfunc  49997  fullthinc2  50036  thincciso  50038  fulltermc2  50097