![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssbri | Structured version Visualization version GIF 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 | . 2 ⊢ 𝐴 ⊆ 𝐵 | |
2 | ssbr 4848 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷)) | |
3 | 1, 2 | ax-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 |