Theorem ssbri 5150

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2836  df-ss 3916  df-br 5104

This theorem is used by:  brel  5716  swoer  8733  swoord1  8734  swoord2  8735  ecopover  8826  endom  8990  brdom3  10588  brdom5  10589  brdom4  10590  fpwwe2lem12  10708  nqerf  10996  nqerrel  10998  isfull  18067  isfth  18071  fulloppc  18079  fthoppc  18080  fthsect  18082  fthinv  18083  fthmon  18084  fthepi  18085  ffthiso  18086  catcisolem  18265  psss  18734  efgrelex  19945  hlimadd  31777  hhsscms  31862  occllem  31887  nlelchi  32645  hmopidmchi  32735  fundmpss  36501  itg2gt0cn  38561  brresi2  38622  imasubc  50203  imasubc2  50204  fthcomf  50209  uptrlem1  50262  uptrlem3  50264  uptr2  50273  fucoppcfunc  50464  fullthinc2  50503  thincciso  50505  fulltermc2  50564