Theorem ssbri 4849

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

Syntax hints:   → wi 4   ⊆ wss 3715   class class class wbr 4804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-in 3722  df-ss 3729  df-br 4805

This theorem is referenced by:  brel  5325  swoer  7941  swoord1  7942  swoord2  7943  ecopover  8018  endom  8148  brdom3  9542  brdom5  9543  brdom4  9544  fpwwe2lem13  9656  nqerf  9944  nqerrel  9946  isfull  16771  isfth  16775  fulloppc  16783  fthoppc  16784  fthsect  16786  fthinv  16787  fthmon  16788  fthepi  16789  ffthiso  16790  catcisolem  16957  psss  17415  efgrelex  18364  hlimadd  28359  hhsscms  28445  occllem  28471  nlelchi  29229  hmopidmchi  29319  fundmpss  31971  itg2gt0cn  33778  brresi  33826