Theorem ssbri 5075

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

Syntax hints:   → wi 4   ⊆ wss 3881   class class class wbr 5030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-br 5031

This theorem is referenced by:  brel  5581  swoer  8302  swoord1  8303  swoord2  8304  ecopover  8384  endom  8519  brdom3  9939  brdom5  9940  brdom4  9941  fpwwe2lem13  10053  nqerf  10341  nqerrel  10343  isfull  17172  isfth  17176  fulloppc  17184  fthoppc  17185  fthsect  17187  fthinv  17188  fthmon  17189  fthepi  17190  ffthiso  17191  catcisolem  17358  psss  17816  efgrelex  18869  hlimadd  28976  hhsscms  29061  occllem  29086  nlelchi  29844  hmopidmchi  29934  fundmpss  33122  itg2gt0cn  35112  brresi2  35157