Theorem ssbri 5155

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

Syntax hints:   → wi 4   ⊆ wss 3917   class class class wbr 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2804  df-ss 3934  df-br 5111

This theorem is referenced by:  brel  5706  swoer  8705  swoord1  8706  swoord2  8707  ecopover  8797  endom  8953  brdom3  10488  brdom5  10489  brdom4  10490  fpwwe2lem12  10602  nqerf  10890  nqerrel  10892  isfull  17881  isfth  17885  fulloppc  17893  fthoppc  17894  fthsect  17896  fthinv  17897  fthmon  17898  fthepi  17899  ffthiso  17900  catcisolem  18079  psss  18546  efgrelex  19688  hlimadd  31129  hhsscms  31214  occllem  31239  nlelchi  31997  hmopidmchi  32087  fundmpss  35761  itg2gt0cn  37676  brresi2  37721  imasubc  49144  imasubc2  49145  fthcomf  49150  uptrlem1  49203  uptrlem3  49205  uptr2  49214  fucoppcfunc  49405  fullthinc2  49444  thincciso  49446  fulltermc2  49505