|   | 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 3989 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ (V × V) → 𝐴 ⊆ (V × V))) | |
| 2 | df-rel 5691 | . 2 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V)) | |
| 3 | df-rel 5691 | . 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) | |
| 4 | 1, 2, 3 | 3imtr4g 296 | 1 ⊢ (𝐴 ⊆ 𝐵 → (Rel 𝐵 → Rel 𝐴)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 Vcvv 3479 ⊆ wss 3950 × cxp 5682 Rel wrel 5689 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 | 
| This theorem depends on definitions: df-bi 207 df-ss 3967 df-rel 5691 | 
| This theorem is referenced by: relin1 5821 relin2 5822 reldif 5824 relres 6022 iss 6052 cnvdif 6162 difxp 6183 sofld 6206 funss 6584 funssres 6609 fliftcnv 7332 fliftfun 7333 releldmdifi 8071 frxp 8152 frxp2 8170 frxp3 8177 reltpos 8257 swoer 8777 sbthcl 9136 fpwwe2lem8 10679 recmulnq 11005 prcdnq 11034 ltrel 11324 lerel 11326 dfle2 13190 dflt2 13191 isinv 17805 invsym2 17808 invfun 17809 oppcsect2 17824 oppcinv 17825 relfull 17956 relfth 17957 psss 18626 gicer 19296 gsum2d 19991 isunit 20374 txdis1cn 23644 hmpher 23793 tgphaus 24126 qustgplem 24130 tsmsxp 24164 xmeter 24444 ovoliunlem1 25538 taylf 26403 lgsquadlem1 27425 lgsquadlem2 27426 noseqrdgfn 28313 nvrel 30622 phrel 30835 bnrel 30887 hlrel 30910 gsumfs2d 33059 elrgspnsubrunlem2 33253 gonan0 35398 sscoid 35915 trer 36318 fneer 36355 heicant 37663 iss2 38346 funALTVss 38701 disjss 38733 dvhopellsm 41120 diclspsn 41197 dih1dimatlem 41332 gricrel 47893 grlicrel 47971 | 
| Copyright terms: Public domain | W3C validator |