![]() |
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 5629 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) | |
2 | dmss 5657 | . . 3 ⊢ (◡𝐴 ⊆ ◡𝐵 → dom ◡𝐴 ⊆ dom ◡𝐵) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 ⊆ 𝐵 → dom ◡𝐴 ⊆ dom ◡𝐵) |
4 | df-rn 5454 | . 2 ⊢ ran 𝐴 = dom ◡𝐴 | |
5 | df-rn 5454 | . 2 ⊢ ran 𝐵 = dom ◡𝐵 | |
6 | 3, 4, 5 | 3sstr4g 3933 | 1 ⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3859 ◡ccnv 5442 dom cdm 5443 ran crn 5444 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-rab 3114 df-v 3439 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-br 4963 df-opab 5025 df-cnv 5451 df-dm 5453 df-rn 5454 |
This theorem is referenced by: rnssi 5692 imass1 5840 imass2 5841 ssxpb 5907 sofld 5920 funssxp 6403 dff2 6728 dff3 6729 fliftf 6931 1stcof 7575 2ndcof 7576 frxp 7673 fodomfi 8643 marypha1lem 8743 marypha1 8744 dfac12lem2 9416 fpwwe2lem13 9910 prdsval 16557 prdsbas 16559 prdsplusg 16560 prdsmulr 16561 prdsvsca 16562 prdshom 16569 catcfuccl 17198 catcxpccl 17286 odf1o2 18428 dprdres 18867 lmss 21590 txss12 21897 txbasval 21898 fmss 22238 tsmsxplem1 22444 ustimasn 22520 utopbas 22527 metustexhalf 22849 causs 23584 ovoliunlem1 23786 dvcnvrelem1 24297 taylf 24632 subgrprop3 26741 sspba 28195 imadifxp 30041 metideq 30750 sxbrsigalem5 31163 omsmon 31173 carsggect 31193 carsgclctunlem2 31194 heicant 34477 mblfinlem1 34479 symrefref2 35349 dicval 37862 rntrclfvOAI 38792 diophrw 38860 dnnumch2 39149 lmhmlnmsplit 39191 hbtlem6 39233 mptrcllem 39477 rntrcl 39492 dfrcl2 39523 relexpss1d 39554 rp-imass 39621 rfovcnvf1od 39854 supcnvlimsup 41582 fourierdlem42 41996 sge0less 42236 |
Copyright terms: Public domain | W3C validator |