![]() |
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 5402 | . 2 ⊢ ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} | |
2 | rnmpt.1 | . . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
3 | df-mpt 4763 | . . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} | |
4 | 2, 3 | eqtri 2673 | . . 3 ⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
5 | 4 | rneqi 5384 | . 2 ⊢ ran 𝐹 = ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
6 | df-rex 2947 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) | |
7 | 6 | abbii 2768 | . 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
8 | 1, 5, 7 | 3eqtr4i 2683 | 1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 383 = wceq 1523 ∃wex 1744 ∈ wcel 2030 {cab 2637 ∃wrex 2942 {copab 4745 ↦ cmpt 4762 ran crn 5144 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-nul 4822 ax-pr 4936 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rex 2947 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-br 4686 df-opab 4746 df-mpt 4763 df-cnv 5151 df-dm 5153 df-rn 5154 |
This theorem is referenced by: elrnmpt 5404 elrnmpt1 5406 elrnmptg 5407 dfiun3g 5410 dfiin3g 5411 fnrnfv 6281 fmpt 6421 fnasrn 6451 fliftf 6605 abrexexg 7182 abrexexOLD 7184 fo1st 7230 fo2nd 7231 qliftf 7878 abrexfi 8307 iinfi 8364 tz9.12lem1 8688 infmap2 9078 cfslb2n 9128 fin23lem29 9201 fin23lem30 9202 fin1a2lem11 9270 ac6num 9339 rankcf 9637 tskuni 9643 negfi 11009 4sqlem11 15706 4sqlem12 15707 vdwapval 15724 vdwlem6 15737 quslem 16250 conjnmzb 17742 pmtrprfvalrn 17954 sylow1lem2 18060 sylow3lem1 18088 sylow3lem2 18089 rnascl 19391 ellspd 20189 iinopn 20755 restco 21016 pnrmopn 21195 cncmp 21243 discmp 21249 comppfsc 21383 alexsublem 21895 ptcmplem3 21905 snclseqg 21966 prdsxmetlem 22220 prdsbl 22343 xrhmeo 22792 pi1xfrf 22899 pi1cof 22905 iunmbl 23367 voliun 23368 itg1addlem4 23511 i1fmulc 23515 mbfi1fseqlem4 23530 itg2monolem1 23562 aannenlem2 24129 2lgslem1b 25162 mptelee 25820 disjrnmpt 29524 ofrn2 29570 abrexct 29622 abrexctf 29624 esumc 30241 esumrnmpt 30242 carsgclctunlem3 30510 eulerpartlemt 30561 bdayfo 31953 nosupno 31974 fobigcup 32132 ptrest 33538 areacirclem2 33631 istotbnd3 33700 sstotbnd 33704 rmxypairf1o 37793 hbtlem6 38016 elrnmptf 39681 fnrnafv 41563 fargshiftfo 41703 |
Copyright terms: Public domain | W3C validator |