Theorem ssbri 5123

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

Syntax hints:   → wi 4   ⊆ wss 3891   class class class wbr 5078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-ss 3908  df-br 5079

This theorem is referenced by:  brel  5651  swoer  8502  swoord1  8503  swoord2  8504  ecopover  8584  endom  8738  brdom3  10268  brdom5  10269  brdom4  10270  fpwwe2lem12  10382  nqerf  10670  nqerrel  10672  isfull  17607  isfth  17611  fulloppc  17619  fthoppc  17620  fthsect  17622  fthinv  17623  fthmon  17624  fthepi  17625  ffthiso  17626  catcisolem  17806  psss  18279  efgrelex  19338  hlimadd  29534  hhsscms  29619  occllem  29644  nlelchi  30402  hmopidmchi  30492  fundmpss  33719  itg2gt0cn  35811  brresi2  35856  fullthinc2  46280  thincciso  46282