Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ssbri | Structured version Visualization version Unicode version |
Description: Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.) |
Ref | Expression |
---|---|
ssbri.1 |
Ref | Expression |
---|---|
ssbri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssbri.1 | . . . 4 | |
2 | 1 | a1i 11 | . . 3 |
3 | 2 | ssbrd 4696 | . 2 |
4 | 3 | trud 1493 | 1 |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |