Theorem ssbri 4896

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

Syntax hints:   → wi 4   ⊆ wss 3776   class class class wbr 4851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2791

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-in 3783  df-ss 3790  df-br 4852

This theorem is referenced by:  brel  5375  swoer  8012  swoord1  8013  swoord2  8014  ecopover  8090  endom  8222  brdom3  9638  brdom5  9639  brdom4  9640  fpwwe2lem13  9752  nqerf  10040  nqerrel  10042  isfull  16777  isfth  16781  fulloppc  16789  fthoppc  16790  fthsect  16792  fthinv  16793  fthmon  16794  fthepi  16795  ffthiso  16796  catcisolem  16963  psss  17422  efgrelex  18368  hlimadd  28384  hhsscms  28470  occllem  28496  nlelchi  29254  hmopidmchi  29344  fundmpss  31991  itg2gt0cn  33779  brresi  33827