![]() |
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 3986 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ (V × V) → 𝐴 ⊆ (V × V))) | |
2 | df-rel 5689 | . 2 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V)) | |
3 | df-rel 5689 | . 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) | |
4 | 1, 2, 3 | 3imtr4g 295 | 1 ⊢ (𝐴 ⊆ 𝐵 → (Rel 𝐵 → Rel 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Vcvv 3462 ⊆ wss 3947 × cxp 5680 Rel wrel 5687 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 |
This theorem depends on definitions: df-bi 206 df-ss 3964 df-rel 5689 |
This theorem is referenced by: relin1 5818 relin2 5819 reldif 5821 relres 6015 iss 6044 cnvdif 6155 difxp 6175 sofld 6198 funss 6578 funssres 6603 fliftcnv 7323 fliftfun 7324 releldmdifi 8059 frxp 8140 frxp2 8158 frxp3 8165 reltpos 8246 swoer 8765 sbthcl 9133 fpwwe2lem8 10681 recmulnq 11007 prcdnq 11036 ltrel 11326 lerel 11328 dfle2 13180 dflt2 13181 isinv 17776 invsym2 17779 invfun 17780 oppcsect2 17795 oppcinv 17796 relfull 17930 relfth 17931 psss 18605 gicer 19271 gsum2d 19970 isunit 20355 txdis1cn 23630 hmpher 23779 tgphaus 24112 qustgplem 24116 tsmsxp 24150 xmeter 24430 ovoliunlem1 25522 taylf 26388 lgsquadlem1 27409 lgsquadlem2 27410 noseqrdgfn 28280 nvrel 30535 phrel 30748 bnrel 30800 hlrel 30823 gonan0 35220 sscoid 35737 trer 36028 fneer 36065 heicant 37356 iss2 38042 funALTVss 38397 disjss 38429 dvhopellsm 40816 diclspsn 40893 dih1dimatlem 41028 gricrel 47467 grlicrel 47496 |
Copyright terms: Public domain | W3C validator |