Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rnss | Structured version Visualization version GIF version |
Description: Subset theorem for range. (Contributed by NM, 22-Mar-1998.) |
Ref | Expression |
---|---|
rnss | ⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvss 5781 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) | |
2 | dmss 5811 | . . 3 ⊢ (◡𝐴 ⊆ ◡𝐵 → dom ◡𝐴 ⊆ dom ◡𝐵) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 ⊆ 𝐵 → dom ◡𝐴 ⊆ dom ◡𝐵) |
4 | df-rn 5600 | . 2 ⊢ ran 𝐴 = dom ◡𝐴 | |
5 | df-rn 5600 | . 2 ⊢ ran 𝐵 = dom ◡𝐵 | |
6 | 3, 4, 5 | 3sstr4g 3966 | 1 ⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3887 ◡ccnv 5588 dom cdm 5589 ran crn 5590 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-br 5075 df-opab 5137 df-cnv 5597 df-dm 5599 df-rn 5600 |
This theorem is referenced by: rnssi 5849 imass1 6009 imass2 6010 ssxpb 6077 sofld 6090 resssxp 6173 funssxp 6629 dff2 6975 dff3 6976 fliftf 7186 1stcof 7861 2ndcof 7862 frxp 7967 fodomfi 9092 marypha1lem 9192 marypha1 9193 dfac12lem2 9900 fpwwe2lem12 10398 prdsvallem 17165 prdsval 17166 prdsbas 17168 prdsplusg 17169 prdsmulr 17170 prdsvsca 17171 prdshom 17178 catcfuccl 17834 catcfucclOLD 17835 catcxpccl 17924 catcxpcclOLD 17925 odf1o2 19178 dprdres 19631 lmss 22449 txss12 22756 txbasval 22757 fmss 23097 tsmsxplem1 23304 ustimasn 23380 utopbas 23387 metustexhalf 23712 causs 24462 ovoliunlem1 24666 dvcnvrelem1 25181 taylf 25520 subgrprop3 27643 sspba 29089 imadifxp 30940 gsumpart 31315 metideq 31843 sxbrsigalem5 32255 omsmon 32265 carsggect 32285 carsgclctunlem2 32286 frxp2 33791 frxp3 33797 heicant 35812 mblfinlem1 35814 symrefref2 36677 dicval 39190 rntrclfvOAI 40513 diophrw 40581 dnnumch2 40870 lmhmlnmsplit 40912 hbtlem6 40954 mptrcllem 41221 rntrcl 41236 dfrcl2 41282 relexpss1d 41313 rfovcnvf1od 41612 supcnvlimsup 43281 fourierdlem42 43690 sge0less 43930 |
Copyright terms: Public domain | W3C validator |