Theorem ssbri 5154

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900   class class class wbr 5106

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2839  df-ss 3901  df-br 5107

This theorem is used by:  brel  5721  swoer  8780  swoord1  8781  swoord2  8782  ecopover  8873  endom  9037  brdom3  10637  brdom5  10638  brdom4  10639  fpwwe2lem12  10757  nqerf  11045  nqerrel  11047  isfull  18119  isfth  18123  fulloppc  18131  fthoppc  18132  fthsect  18134  fthinv  18135  fthmon  18136  fthepi  18137  ffthiso  18138  catcisolem  18317  psss  18786  efgrelex  19998  hlimadd  31828  hhsscms  31913  occllem  31938  nlelchi  32696  hmopidmchi  32786  fundmpss  36723  itg2gt0cn  38798  brresi2  38859  imasubc  50482  imasubc2  50483  fthcomf  50488  uptrlem1  50541  uptrlem3  50543  uptr2  50552  fucoppcfunc  50762  fullthinc2  50801  thincciso  50803  fulltermc2  50862