![]() |
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 5193 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶𝐴𝐷 → 𝐶𝐵𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3944 class class class wbr 5149 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-clel 2802 df-ss 3961 df-br 5150 |
This theorem is referenced by: brel 5743 swoer 8755 swoord1 8756 swoord2 8757 ecopover 8840 endom 9000 brdom3 10553 brdom5 10554 brdom4 10555 fpwwe2lem12 10667 nqerf 10955 nqerrel 10957 isfull 17902 isfth 17906 fulloppc 17914 fthoppc 17915 fthsect 17917 fthinv 17918 fthmon 17919 fthepi 17920 ffthiso 17921 catcisolem 18102 psss 18575 efgrelex 19718 hlimadd 31075 hhsscms 31160 occllem 31185 nlelchi 31943 hmopidmchi 32033 fundmpss 35493 itg2gt0cn 37279 brresi2 37324 fullthinc2 48239 thincciso 48241 |
Copyright terms: Public domain | W3C validator |