![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > relss | Structured version Visualization version GIF version |
Description: Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58. (Contributed by NM, 15-Aug-1994.) |
Ref | Expression |
---|---|
relss | ⊢ (𝐴 ⊆ 𝐵 → (Rel 𝐵 → Rel 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sstr2 3865 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ (V × V) → 𝐴 ⊆ (V × V))) | |
2 | df-rel 5414 | . 2 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V)) | |
3 | df-rel 5414 | . 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) | |
4 | 1, 2, 3 | 3imtr4g 288 | 1 ⊢ (𝐴 ⊆ 𝐵 → (Rel 𝐵 → Rel 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Vcvv 3415 ⊆ wss 3829 × cxp 5405 Rel wrel 5412 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-in 3836 df-ss 3843 df-rel 5414 |
This theorem is referenced by: relin1 5535 relin2 5536 reldif 5538 relres 5727 iss 5748 cnvdif 5842 difxp 5861 sofld 5884 funss 6207 funssres 6231 fliftcnv 6887 fliftfun 6888 frxp 7625 reltpos 7700 swoer 8119 sbthcl 8435 fpwwe2lem9 9858 recmulnq 10184 prcdnq 10213 ltrel 10503 lerel 10505 dfle2 12357 dflt2 12358 isinv 16888 invsym2 16891 invfun 16892 oppcsect2 16907 oppcinv 16908 relfull 17036 relfth 17037 psss 17682 gicer 18187 gsum2d 18845 isunit 19130 txdis1cn 21947 hmpher 22096 tgphaus 22428 qustgplem 22432 tsmsxp 22466 xmeter 22746 ovoliunlem1 23806 taylf 24652 lgsquadlem1 25658 lgsquadlem2 25659 nvrel 28156 phrel 28369 bnrel 28422 hlrel 28445 sscoid 32901 trer 33191 fneer 33228 heicant 34374 iss2 35053 funALTVss 35383 disjss 35415 dvhopellsm 37704 diclspsn 37781 dih1dimatlem 37916 |
Copyright terms: Public domain | W3C validator |