Theorem ssbri 4697

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 4696	. 2 ⊢ (⊤ → (𝐶𝐴𝐷 → 𝐶𝐵𝐷))
4	3	trud 1493	1 ⊢ (𝐶𝐴𝐷 → 𝐶𝐵𝐷)

Syntax hints:   → wi 4  ⊤wtru 1484   ⊆ wss 3574   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588  df-br 4654

This theorem is referenced by:  brel  5168  swoer  7772  swoord1  7773  swoord2  7774  ecopover  7851  ecopoverOLD  7852  endom  7982  brdom3  9350  brdom5  9351  brdom4  9352  fpwwe2lem13  9464  nqerf  9752  nqerrel  9754  isfull  16570  isfth  16574  fulloppc  16582  fthoppc  16583  fthsect  16585  fthinv  16586  fthmon  16587  fthepi  16588  ffthiso  16589  catcisolem  16756  psss  17214  efgrelex  18164  hlimadd  28050  hhsscms  28136  occllem  28162  nlelchi  28920  hmopidmchi  29010  fundmpss  31664  itg2gt0cn  33465  brresi  33513