![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rnmpt | Structured version Visualization version Unicode version |
Description: The range of a function in maps-to notation. (Contributed by Scott Fenton, 21-Mar-2011.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Ref | Expression |
---|---|
rnmpt.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
rnmpt |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rnopab 5097 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | rnmpt.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | df-mpt 4476 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | eqtri 2483 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | rneqi 5079 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | df-rex 2754 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 6 | abbii 2577 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 1, 5, 7 | 3eqtr4i 2493 |
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 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-9 1906 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-sep 4538 ax-nul 4547 ax-pr 4652 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-eu 2313 df-mo 2314 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-rex 2754 df-rab 2757 df-v 3058 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-nul 3743 df-if 3893 df-sn 3980 df-pr 3982 df-op 3986 df-br 4416 df-opab 4475 df-mpt 4476 df-cnv 4860 df-dm 4862 df-rn 4863 |
This theorem is referenced by: elrnmpt 5099 elrnmpt1 5101 elrnmptg 5102 dfiun3g 5105 dfiin3g 5106 fnrnfv 5933 fmpt 6065 fnasrn 6093 fliftf 6232 abrexex 6793 abrexexg 6794 fo1st 6839 fo2nd 6840 qliftf 7476 abrexfi 7899 iinfi 7956 tz9.12lem1 8283 infmap2 8673 cfslb2n 8723 fin23lem29 8796 fin23lem30 8797 fin1a2lem11 8865 ac6num 8934 rankcf 9227 tskuni 9233 negfi 10581 4sqlem11 14947 4sqlem12 14948 vdwapval 14971 vdwlem6 14984 quslem 15497 conjnmzb 16965 pmtrprfvalrn 17177 sylow1lem2 17299 sylow3lem1 17327 sylow3lem2 17328 rnascl 18615 ellspd 19408 iinopn 19980 restco 20228 pnrmopn 20407 cncmp 20455 discmp 20461 comppfsc 20595 alexsublem 21107 ptcmplem3 21117 snclseqg 21178 prdsxmetlem 21431 prdsbl 21554 xrhmeo 22022 pi1xfrf 22132 pi1cof 22138 iunmbl 22554 voliun 22555 itg1addlem4 22705 i1fmulc 22709 mbfi1fseqlem4 22724 itg2monolem1 22756 aannenlem2 23333 mptelee 24973 nbgraf1olem5 25221 fargshiftfo 25414 efghgrpOLD 26149 circgrpOLD 26150 disjrnmpt 28243 ofrn2 28289 abrexct 28352 abrexctf 28354 esumc 28920 esumrnmpt 28921 carsgclctunlem3 29200 eulerpartlemt 29252 bdayfo 30612 fobigcup 30715 ptrest 31983 areacirclem2 32077 istotbnd3 32147 sstotbnd 32151 rmxypairf1o 35803 hbtlem6 36032 elrnmptf 37491 fnrnafv 38701 |
Copyright terms: Public domain | W3C validator |