Theorem ssbri 5154

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3902   class class class wbr 5107

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 2837  df-ss 3919  df-br 5108

This theorem is used by:  brel  5724  swoer  8732  swoord1  8733  swoord2  8734  ecopover  8825  endom  8989  brdom3  10535  brdom5  10536  brdom4  10537  fpwwe2lem12  10655  nqerf  10943  nqerrel  10945  isfull  18007  isfth  18011  fulloppc  18019  fthoppc  18020  fthsect  18022  fthinv  18023  fthmon  18024  fthepi  18025  ffthiso  18026  catcisolem  18205  psss  18674  efgrelex  19884  hlimadd  31682  hhsscms  31767  occllem  31792  nlelchi  32550  hmopidmchi  32640  fundmpss  36354  itg2gt0cn  38432  brresi2  38478  imasubc  50085  imasubc2  50086  fthcomf  50091  uptrlem1  50144  uptrlem3  50146  uptr2  50155  fucoppcfunc  50346  fullthinc2  50385  thincciso  50387  fulltermc2  50446