Theorem ssbri 5111

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

Syntax hints:   → wi 4   ⊆ wss 3936   class class class wbr 5066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952  df-br 5067

This theorem is referenced by:  brel  5617  swoer  8319  swoord1  8320  swoord2  8321  ecopover  8401  endom  8536  brdom3  9950  brdom5  9951  brdom4  9952  fpwwe2lem13  10064  nqerf  10352  nqerrel  10354  isfull  17180  isfth  17184  fulloppc  17192  fthoppc  17193  fthsect  17195  fthinv  17196  fthmon  17197  fthepi  17198  ffthiso  17199  catcisolem  17366  psss  17824  efgrelex  18877  hlimadd  28970  hhsscms  29055  occllem  29080  nlelchi  29838  hmopidmchi  29928  fundmpss  33009  itg2gt0cn  34962  brresi2  35009