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

Theorem ssbri 4494
 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 . . . 4
21a1i 11 . . 3
32ssbrd 4493 . 2
43trud 1404 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4   wtru 1396  C_wss 3475   class class class wbr 4452 This theorem is referenced by:  brel  5053  swoer  7358  swoord1  7359  swoord2  7360  ecopover  7434  endom  7562  brdom3  8927  brdom5  8928  brdom4  8929  fpwwe2lem13  9041  nqerf  9329  nqerrel  9331  isfull  15279  isfth  15283  fulloppc  15291  fthoppc  15292  fthsect  15294  fthinv  15295  fthmon  15296  fthepi  15297  ffthiso  15298  catcisolem  15433  psss  15844  efgrelex  16769  hlimadd  26110  hhsscms  26195  occllem  26221  nlelchi  26980  hmopidmchi  27070  fundmpss  29196  itg2gt0cn  30070  brresi  30209 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489  df-br 4453
 Copyright terms: Public domain W3C validator