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 5726 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) | |
2 | dmss 5756 | . . 3 ⊢ (◡𝐴 ⊆ ◡𝐵 → dom ◡𝐴 ⊆ dom ◡𝐵) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 ⊆ 𝐵 → dom ◡𝐴 ⊆ dom ◡𝐵) |
4 | df-rn 5547 | . 2 ⊢ ran 𝐴 = dom ◡𝐴 | |
5 | df-rn 5547 | . 2 ⊢ ran 𝐵 = dom ◡𝐵 | |
6 | 3, 4, 5 | 3sstr4g 3932 | 1 ⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3853 ◡ccnv 5535 dom cdm 5536 ran crn 5537 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-rab 3060 df-v 3400 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4224 df-if 4426 df-sn 4528 df-pr 4530 df-op 4534 df-br 5040 df-opab 5102 df-cnv 5544 df-dm 5546 df-rn 5547 |
This theorem is referenced by: rnssi 5794 imass1 5949 imass2 5950 ssxpb 6017 sofld 6030 resssxp 6113 funssxp 6552 dff2 6896 dff3 6897 fliftf 7102 1stcof 7769 2ndcof 7770 frxp 7871 fodomfi 8927 marypha1lem 9027 marypha1 9028 dfac12lem2 9723 fpwwe2lem12 10221 prdsvallem 16913 prdsval 16914 prdsbas 16916 prdsplusg 16917 prdsmulr 16918 prdsvsca 16919 prdshom 16926 catcfuccl 17579 catcfucclOLD 17580 catcxpccl 17668 catcxpcclOLD 17669 odf1o2 18916 dprdres 19369 lmss 22149 txss12 22456 txbasval 22457 fmss 22797 tsmsxplem1 23004 ustimasn 23080 utopbas 23087 metustexhalf 23408 causs 24149 ovoliunlem1 24353 dvcnvrelem1 24868 taylf 25207 subgrprop3 27318 sspba 28762 imadifxp 30613 gsumpart 30988 metideq 31511 sxbrsigalem5 31921 omsmon 31931 carsggect 31951 carsgclctunlem2 31952 frxp2 33471 frxp3 33477 heicant 35498 mblfinlem1 35500 symrefref2 36363 dicval 38876 rntrclfvOAI 40157 diophrw 40225 dnnumch2 40514 lmhmlnmsplit 40556 hbtlem6 40598 mptrcllem 40838 rntrcl 40853 dfrcl2 40900 relexpss1d 40931 rfovcnvf1od 41230 supcnvlimsup 42899 fourierdlem42 43308 sge0less 43548 |
Copyright terms: Public domain | W3C validator |