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 3913   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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-br 5111

This theorem is referenced by:  brel  5702  swoer  8685  swoord1  8686  swoord2  8687  ecopover  8767  endom  8926  brdom3  10473  brdom5  10474  brdom4  10475  fpwwe2lem12  10587  nqerf  10875  nqerrel  10877  isfull  17811  isfth  17815  fulloppc  17823  fthoppc  17824  fthsect  17826  fthinv  17827  fthmon  17828  fthepi  17829  ffthiso  17830  catcisolem  18010  psss  18483  efgrelex  19547  hlimadd  30198  hhsscms  30283  occllem  30308  nlelchi  31066  hmopidmchi  31156  fundmpss  34427  itg2gt0cn  36206  brresi2  36251  fullthinc2  47187  thincciso  47189