Theorem ssbri 4657

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	. . . 4 ⊢ 𝐴 ⊆ 𝐵
2	1	a1i 11	. . 3 ⊢ (⊤ → 𝐴 ⊆ 𝐵)
3	2	ssbrd 4656	. 2 ⊢ (⊤ → (𝐶𝐴𝐷 → 𝐶𝐵𝐷))
4	3	trud 1490	1 ⊢ (𝐶𝐴𝐷 → 𝐶𝐵𝐷)

Syntax hints:   → wi 4  ⊤wtru 1481   ⊆ wss 3555   class class class wbr 4613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3562  df-ss 3569  df-br 4614

This theorem is referenced by:  brel  5128  swoer  7717  swoord1  7718  swoord2  7719  ecopover  7796  ecopoverOLD  7797  endom  7926  brdom3  9294  brdom5  9295  brdom4  9296  fpwwe2lem13  9408  nqerf  9696  nqerrel  9698  isfull  16491  isfth  16495  fulloppc  16503  fthoppc  16504  fthsect  16506  fthinv  16507  fthmon  16508  fthepi  16509  ffthiso  16510  catcisolem  16677  psss  17135  efgrelex  18085  hlimadd  27896  hhsscms  27982  occllem  28008  nlelchi  28766  hmopidmchi  28856  fundmpss  31365  itg2gt0cn  33094  brresi  33142