Theorem ssbri 5126

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

Syntax hints:   → wi 4   ⊆ wss 3892   class class class wbr 5081

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-in 3899  df-ss 3909  df-br 5082

This theorem is referenced by:  brel  5663  swoer  8559  swoord1  8560  swoord2  8561  ecopover  8641  endom  8800  brdom3  10334  brdom5  10335  brdom4  10336  fpwwe2lem12  10448  nqerf  10736  nqerrel  10738  isfull  17675  isfth  17679  fulloppc  17687  fthoppc  17688  fthsect  17690  fthinv  17691  fthmon  17692  fthepi  17693  ffthiso  17694  catcisolem  17874  psss  18347  efgrelex  19406  hlimadd  29604  hhsscms  29689  occllem  29714  nlelchi  30472  hmopidmchi  30562  fundmpss  33789  itg2gt0cn  35880  brresi2  35925  fullthinc2  46572  thincciso  46574