Theorem ssbri 4627

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

Syntax hints:   → wi 4  ⊤wtru 1476   ⊆ wss 3540   class class class wbr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-br 4584

This theorem is referenced by:  brel  5090  swoer  7659  swoord1  7660  swoord2  7661  ecopover  7738  ecopoverOLD  7739  endom  7868  brdom3  9231  brdom5  9232  brdom4  9233  fpwwe2lem13  9343  nqerf  9631  nqerrel  9633  isfull  16393  isfth  16397  fulloppc  16405  fthoppc  16406  fthsect  16408  fthinv  16409  fthmon  16410  fthepi  16411  ffthiso  16412  catcisolem  16579  psss  17037  efgrelex  17987  hlimadd  27434  hhsscms  27520  occllem  27546  nlelchi  28304  hmopidmchi  28394  fundmpss  30910  itg2gt0cn  32635  brresi  32683