MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssbri Structured version   Visualization version   GIF version

Theorem ssbri 4849
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
StepHypRef Expression
1 ssbri.1 . 2 𝐴𝐵
2 ssbr 4848 . 2 (𝐴𝐵 → (𝐶𝐴𝐷𝐶𝐵𝐷))
31, 2ax-mp 5 1 (𝐶𝐴𝐷𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3715   class class class wbr 4804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-in 3722  df-ss 3729  df-br 4805
This theorem is referenced by:  brel  5325  swoer  7941  swoord1  7942  swoord2  7943  ecopover  8018  endom  8148  brdom3  9542  brdom5  9543  brdom4  9544  fpwwe2lem13  9656  nqerf  9944  nqerrel  9946  isfull  16771  isfth  16775  fulloppc  16783  fthoppc  16784  fthsect  16786  fthinv  16787  fthmon  16788  fthepi  16789  ffthiso  16790  catcisolem  16957  psss  17415  efgrelex  18364  hlimadd  28359  hhsscms  28445  occllem  28471  nlelchi  29229  hmopidmchi  29319  fundmpss  31971  itg2gt0cn  33778  brresi  33826
  Copyright terms: Public domain W3C validator