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 5737 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) | |
2 | dmss 5765 | . . 3 ⊢ (◡𝐴 ⊆ ◡𝐵 → dom ◡𝐴 ⊆ dom ◡𝐵) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 ⊆ 𝐵 → dom ◡𝐴 ⊆ dom ◡𝐵) |
4 | df-rn 5560 | . 2 ⊢ ran 𝐴 = dom ◡𝐴 | |
5 | df-rn 5560 | . 2 ⊢ ran 𝐵 = dom ◡𝐵 | |
6 | 3, 4, 5 | 3sstr4g 4011 | 1 ⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3935 ◡ccnv 5548 dom cdm 5549 ran crn 5550 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3497 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-br 5059 df-opab 5121 df-cnv 5557 df-dm 5559 df-rn 5560 |
This theorem is referenced by: rnssi 5804 imass1 5958 imass2 5959 ssxpb 6025 sofld 6038 funssxp 6529 dff2 6858 dff3 6859 fliftf 7057 1stcof 7710 2ndcof 7711 frxp 7811 fodomfi 8786 marypha1lem 8886 marypha1 8887 dfac12lem2 9559 fpwwe2lem13 10053 prdsval 16718 prdsbas 16720 prdsplusg 16721 prdsmulr 16722 prdsvsca 16723 prdshom 16730 catcfuccl 17359 catcxpccl 17447 odf1o2 18629 dprdres 19081 lmss 21836 txss12 22143 txbasval 22144 fmss 22484 tsmsxplem1 22690 ustimasn 22766 utopbas 22773 metustexhalf 23095 causs 23830 ovoliunlem1 24032 dvcnvrelem1 24543 taylf 24878 subgrprop3 26986 sspba 28432 imadifxp 30280 metideq 31033 sxbrsigalem5 31446 omsmon 31456 carsggect 31476 carsgclctunlem2 31477 heicant 34809 mblfinlem1 34811 symrefref2 35681 dicval 38194 rntrclfvOAI 39168 diophrw 39236 dnnumch2 39525 lmhmlnmsplit 39567 hbtlem6 39609 mptrcllem 39853 rntrcl 39868 dfrcl2 39899 relexpss1d 39930 rp-imass 39997 rfovcnvf1od 40230 supcnvlimsup 41901 fourierdlem42 42315 sge0less 42555 |
Copyright terms: Public domain | W3C validator |