![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rnss | Structured version Visualization version Unicode version |
Description: Subset theorem for range. (Contributed by NM, 22-Mar-1998.) |
Ref | Expression |
---|---|
rnss |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvss 5010 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | dmss 5037 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 17 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | df-rn 4848 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | df-rn 4848 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | 3sstr4g 3475 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-rab 2748 df-v 3049 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-nul 3734 df-if 3884 df-sn 3971 df-pr 3973 df-op 3977 df-br 4406 df-opab 4465 df-cnv 4845 df-dm 4847 df-rn 4848 |
This theorem is referenced by: imass1 5206 imass2 5207 ssxpb 5274 ssrnres 5278 sofld 5287 funssxp 5747 fssres 5754 dff2 6039 dff3 6040 fliftf 6213 1stcof 6826 2ndcof 6827 frxp 6911 smores 7076 fodomfi 7855 marypha1lem 7952 marypha1 7953 dfac12lem2 8579 brdom4 8963 smobeth 9016 fpwwe2lem13 9072 nqerf 9360 prdsval 15365 prdsbas 15367 prdsplusg 15368 prdsmulr 15369 prdsvsca 15370 prdshom 15377 catcoppccl 16015 catcfuccl 16016 catcxpccl 16104 lern 16483 odf1o2 17234 gsumzres 17555 gsumzaddlem 17566 gsumzadd 17567 dprdfadd 17665 dprdres 17673 lmss 20326 txss12 20632 txbasval 20633 txkgen 20679 fmss 20973 tsmsxplem1 21179 ustimasn 21255 utopbas 21262 metustexhalf 21583 causs 22280 ovoliunlem1 22467 dvcnvrelem1 22981 taylf 23328 dvlog 23608 perpln2 24768 sspba 26378 imadifxp 28224 metideq 28708 sxbrsigalem5 29122 omsmon 29138 omsmonOLD 29142 carsggect 29162 carsgclctunlem2 29163 nodenselem6 30587 fixssrn 30686 heicant 31987 mblfinlem1 31989 dicval 34756 rntrclfvOAI 35545 diophrw 35613 dnnumch2 35915 lmhmlnmsplit 35957 hbtlem6 36000 mptrcllem 36232 cnvrcl0 36244 rntrcl 36247 dfrcl2 36278 relexpss1d 36309 rp-imass 36378 rnresss 37461 fourierdlem42 38022 fourierdlem42OLD 38023 sge0less 38244 subgrprop3 39358 |
Copyright terms: Public domain | W3C validator |