Theorem ssbri 5149

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3895   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835  df-ss 3896  df-br 5103

This theorem is used by:  brel  5715  swoer  8752  swoord1  8753  swoord2  8754  ecopover  8845  endom  9009  brdom3  10610  brdom5  10611  brdom4  10612  fpwwe2lem12  10730  nqerf  11018  nqerrel  11020  isfull  18092  isfth  18096  fulloppc  18104  fthoppc  18105  fthsect  18107  fthinv  18108  fthmon  18109  fthepi  18110  ffthiso  18111  catcisolem  18290  psss  18759  efgrelex  19970  hlimadd  31800  hhsscms  31885  occllem  31910  nlelchi  32668  hmopidmchi  32758  fundmpss  36624  itg2gt0cn  38686  brresi2  38747  imasubc  50360  imasubc2  50361  fthcomf  50366  uptrlem1  50419  uptrlem3  50421  uptr2  50430  fucoppcfunc  50640  fullthinc2  50679  thincciso  50681  fulltermc2  50740