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 5370 | . 2 | |
2 | rnmpt.1 | . . . 4 | |
3 | df-mpt 4730 | . . . 4 | |
4 | 2, 3 | eqtri 2644 | . . 3 |
5 | 4 | rneqi 5352 | . 2 |
6 | df-rex 2918 | . . 3 | |
7 | 6 | abbii 2739 | . 2 |
8 | 1, 5, 7 | 3eqtr4i 2654 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wa 384 wceq 1483 wex 1704 wcel 1990 cab 2608 wrex 2913 copab 4712 cmpt 4729 crn 5115 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-br 4654 df-opab 4713 df-mpt 4730 df-cnv 5122 df-dm 5124 df-rn 5125 |
This theorem is referenced by: elrnmpt 5372 elrnmpt1 5374 elrnmptg 5375 dfiun3g 5378 dfiin3g 5379 fnrnfv 6242 fmpt 6381 fnasrn 6411 fliftf 6565 abrexexg 7140 abrexexOLD 7142 fo1st 7188 fo2nd 7189 qliftf 7835 abrexfi 8266 iinfi 8323 tz9.12lem1 8650 infmap2 9040 cfslb2n 9090 fin23lem29 9163 fin23lem30 9164 fin1a2lem11 9232 ac6num 9301 rankcf 9599 tskuni 9605 negfi 10971 4sqlem11 15659 4sqlem12 15660 vdwapval 15677 vdwlem6 15690 quslem 16203 conjnmzb 17695 pmtrprfvalrn 17908 sylow1lem2 18014 sylow3lem1 18042 sylow3lem2 18043 rnascl 19343 ellspd 20141 iinopn 20707 restco 20968 pnrmopn 21147 cncmp 21195 discmp 21201 comppfsc 21335 alexsublem 21848 ptcmplem3 21858 snclseqg 21919 prdsxmetlem 22173 prdsbl 22296 xrhmeo 22745 pi1xfrf 22853 pi1cof 22859 iunmbl 23321 voliun 23322 itg1addlem4 23466 i1fmulc 23470 mbfi1fseqlem4 23485 itg2monolem1 23517 aannenlem2 24084 2lgslem1b 25117 mptelee 25775 disjrnmpt 29398 ofrn2 29442 abrexct 29494 abrexctf 29496 esumc 30113 esumrnmpt 30114 carsgclctunlem3 30382 eulerpartlemt 30433 bdayfo 31828 nosupno 31849 fobigcup 32007 ptrest 33408 areacirclem2 33501 istotbnd3 33570 sstotbnd 33574 rmxypairf1o 37476 hbtlem6 37699 elrnmptf 39367 fnrnafv 41242 fargshiftfo 41378 |
Copyright terms: Public domain | W3C validator |