![]() |
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 5870 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) | |
2 | dmss 5900 | . . 3 ⊢ (◡𝐴 ⊆ ◡𝐵 → dom ◡𝐴 ⊆ dom ◡𝐵) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 ⊆ 𝐵 → dom ◡𝐴 ⊆ dom ◡𝐵) |
4 | df-rn 5684 | . 2 ⊢ ran 𝐴 = dom ◡𝐴 | |
5 | df-rn 5684 | . 2 ⊢ ran 𝐵 = dom ◡𝐵 | |
6 | 3, 4, 5 | 3sstr4g 4024 | 1 ⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3945 ◡ccnv 5672 dom cdm 5673 ran crn 5674 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-rab 3429 df-v 3472 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-nul 4320 df-if 4526 df-sn 4626 df-pr 4628 df-op 4632 df-br 5144 df-opab 5206 df-cnv 5681 df-dm 5683 df-rn 5684 |
This theorem is referenced by: rnssi 5937 imass1 6100 imass2 6101 ssxpb 6173 sofld 6186 resssxp 6269 funssxp 6747 dff2 7104 dff3 7105 fliftf 7318 1stcof 8018 2ndcof 8019 frxp 8126 frxp2 8144 frxp3 8151 fodomfi 9344 marypha1lem 9451 marypha1 9452 dfac12lem2 10162 fpwwe2lem12 10660 prdsvallem 17430 prdsval 17431 prdsbas 17433 prdsplusg 17434 prdsmulr 17435 prdsvsca 17436 prdshom 17443 catcfuccl 18102 catcfucclOLD 18103 catcxpccl 18192 catcxpcclOLD 18193 odf1o2 19522 dprdres 19979 lmss 23196 txss12 23503 txbasval 23504 fmss 23844 tsmsxplem1 24051 ustimasn 24127 utopbas 24134 metustexhalf 24459 causs 25220 ovoliunlem1 25425 dvcnvrelem1 25944 taylf 26289 subgrprop3 29083 sspba 30531 imadifxp 32385 gsumpart 32764 metideq 33489 sxbrsigalem5 33903 omsmon 33913 carsggect 33933 carsgclctunlem2 33934 heicant 37123 mblfinlem1 37125 symrefref2 38030 dicval 40644 aks6d1c2 41596 rntrclfvOAI 42102 diophrw 42170 dnnumch2 42460 lmhmlnmsplit 42502 hbtlem6 42544 mptrcllem 43034 rntrcl 43049 dfrcl2 43095 relexpss1d 43126 rfovcnvf1od 43425 supcnvlimsup 45119 fourierdlem42 45528 sge0less 45771 |
Copyright terms: Public domain | W3C validator |