Theorem ssbri 5195

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

Syntax hints:   → wi 4   ⊆ wss 3947   class class class wbr 5150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3473  df-in 3954  df-ss 3964  df-br 5151

This theorem is referenced by:  brel  5745  swoer  8759  swoord1  8760  swoord2  8761  ecopover  8844  endom  9004  brdom3  10557  brdom5  10558  brdom4  10559  fpwwe2lem12  10671  nqerf  10959  nqerrel  10961  isfull  17904  isfth  17908  fulloppc  17916  fthoppc  17917  fthsect  17919  fthinv  17920  fthmon  17921  fthepi  17922  ffthiso  17923  catcisolem  18104  psss  18577  efgrelex  19711  hlimadd  31021  hhsscms  31106  occllem  31131  nlelchi  31889  hmopidmchi  31979  fundmpss  35367  itg2gt0cn  37153  brresi2  37198  fullthinc2  48104  thincciso  48106