Theorem ssbri 5161

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3908   class class class wbr 5114

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 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2841  df-ss 3925  df-br 5115

This theorem is used by:  brel  5731  swoer  8735  swoord1  8736  swoord2  8737  ecopover  8828  endom  8985  brdom3  10530  brdom5  10531  brdom4  10532  fpwwe2lem12  10645  nqerf  10933  nqerrel  10935  isfull  17994  isfth  17998  fulloppc  18006  fthoppc  18007  fthsect  18009  fthinv  18010  fthmon  18011  fthepi  18012  ffthiso  18013  catcisolem  18192  psss  18661  efgrelex  19852  hlimadd  31582  hhsscms  31667  occllem  31692  nlelchi  32450  hmopidmchi  32540  fundmpss  36280  itg2gt0cn  38367  brresi2  38412  imasubc  49970  imasubc2  49971  fthcomf  49976  uptrlem1  50029  uptrlem3  50031  uptr2  50040  fucoppcfunc  50231  fullthinc2  50270  thincciso  50272  fulltermc2  50331