| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rnmpt | Structured version Visualization version GIF 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 | ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rnopab 5965 | . 2 ⊢ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} | |
| 2 | rnmpt.1 | . . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
| 3 | df-mpt 5226 | . . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} | |
| 4 | 2, 3 | eqtri 2765 | . . 3 ⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
| 5 | 4 | rneqi 5948 | . 2 ⊢ ran 𝐹 = ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
| 6 | df-rex 3071 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) | |
| 7 | 6 | abbii 2809 | . 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
| 8 | 1, 5, 7 | 3eqtr4i 2775 | 1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 395 = wceq 1540 ∃wex 1779 ∈ wcel 2108 {cab 2714 ∃wrex 3070 {copab 5205 ↦ cmpt 5225 ran crn 5686 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 df-opab 5206 df-mpt 5226 df-cnv 5693 df-dm 5695 df-rn 5696 |
| This theorem is referenced by: elrnmpt 5969 elrnmpt1 5971 elrnmptg 5972 dfiun3g 5978 dfiin3g 5979 fnrnfv 6968 fmpt 7130 fnasrn 7165 fliftf 7335 abrexexgOLD 7986 fo1st 8034 fo2nd 8035 fsplitfpar 8143 qliftf 8845 abrexfi 9392 iinfi 9457 tz9.12lem1 9827 infmap2 10257 cfslb2n 10308 fin23lem29 10381 fin23lem30 10382 fin1a2lem11 10450 ac6num 10519 rankcf 10817 tskuni 10823 negfi 12217 4sqlem11 16993 4sqlem12 16994 vdwapval 17011 vdwlem6 17024 quslem 17588 smndex2dnrinv 18928 conjnmzb 19271 pmtrprfvalrn 19506 sylow1lem2 19617 sylow3lem1 19645 sylow3lem2 19646 ablsimpgfind 20130 pzriprnglem10 21501 ellspd 21822 rnascl 21911 iinopn 22908 restco 23172 pnrmopn 23351 cncmp 23400 discmp 23406 comppfsc 23540 alexsublem 24052 ptcmplem3 24062 snclseqg 24124 prdsxmetlem 24378 prdsbl 24504 xrhmeo 24977 pi1xfrf 25086 pi1cof 25092 iunmbl 25588 voliun 25589 itg1addlem4 25734 i1fmulc 25738 mbfi1fseqlem4 25753 itg2monolem1 25785 aannenlem2 26371 2lgslem1b 27436 bdayfo 27722 nosupno 27748 noinfno 27763 addsuniflem 28034 mptelee 28910 disjrnmpt 32598 ofrn2 32650 abrexct 32728 abrexctf 32730 qusbas2 33434 nsgqusf1olem2 33442 esumc 34052 esumrnmpt 34053 carsgclctunlem3 34322 eulerpartlemt 34373 fobigcup 35901 ptrest 37626 areacirclem2 37716 istotbnd3 37778 sstotbnd 37782 dfqs2 42278 rnasclg 42509 rmxypairf1o 42923 hbtlem6 43141 onsucrn 43284 elrnmptf 45186 fnrnafv 47174 fundcmpsurinjlem1 47385 imasetpreimafvbijlemfo 47392 fargshiftfo 47429 |
| Copyright terms: Public domain | W3C validator |