| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ssbrd | Structured version Visualization version GIF version | ||
| Description: Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.) |
| Ref | Expression |
|---|---|
| ssbrd.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
| Ref | Expression |
|---|---|
| ssbrd | ⊢ (𝜑 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssbrd.1 | . . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
| 2 | 1 | sseld 3982 | . 2 ⊢ (𝜑 → (〈𝐶, 𝐷〉 ∈ 𝐴 → 〈𝐶, 𝐷〉 ∈ 𝐵)) |
| 3 | df-br 5144 | . 2 ⊢ (𝐶𝐴𝐷 ↔ 〈𝐶, 𝐷〉 ∈ 𝐴) | |
| 4 | df-br 5144 | . 2 ⊢ (𝐶𝐵𝐷 ↔ 〈𝐶, 𝐷〉 ∈ 𝐵) | |
| 5 | 2, 3, 4 | 3imtr4g 296 | 1 ⊢ (𝜑 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 ⊆ wss 3951 〈cop 4632 class class class wbr 5143 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-clel 2816 df-ss 3968 df-br 5144 |
| This theorem is referenced by: ssbr 5187 sess1 5650 brrelex12 5737 eqbrrdva 5880 predtrss 6343 ersym 8757 ertr 8760 ttrclss 9760 fpwwe2lem5 10675 fpwwe2lem6 10676 fpwwe2lem8 10678 fpwwe2lem11 10681 fpwwe2lem12 10682 fpwwe2 10683 coss12d 15011 fthres2 17979 invfuc 18022 pospo 18390 dirref 18646 efgcpbl 19774 frgpuplem 19790 subrguss 20587 znleval 21573 ustref 24227 ustuqtop4 24253 metider 33893 mclsppslem 35588 fundmpss 35767 eqvrelsym 38606 eqvreltr 38608 iunrelexpuztr 43732 frege96d 43762 frege91d 43764 frege98d 43766 frege124d 43774 grucollcld 44279 |
| Copyright terms: Public domain | W3C validator |