Theorem ssbri 5124

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

Syntax hints:   → wi 4   ⊆ wss 3890   class class class wbr 5079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clel 2815  df-ss 3907  df-br 5080

This theorem is referenced by:  brel  5690  swoer  8672  swoord1  8673  swoord2  8674  ecopover  8765  endom  8923  brdom3  10448  brdom5  10449  brdom4  10450  fpwwe2lem12  10563  nqerf  10851  nqerrel  10853  isfull  17877  isfth  17881  fulloppc  17889  fthoppc  17890  fthsect  17892  fthinv  17893  fthmon  17894  fthepi  17895  ffthiso  17896  catcisolem  18075  psss  18544  efgrelex  19724  hlimadd  31289  hhsscms  31374  occllem  31399  nlelchi  32157  hmopidmchi  32247  fundmpss  36002  itg2gt0cn  38049  brresi2  38094  imasubc  49648  imasubc2  49649  fthcomf  49654  uptrlem1  49707  uptrlem3  49709  uptr2  49718  fucoppcfunc  49909  fullthinc2  49948  thincciso  49950  fulltermc2  50009