| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > fmpti | Structured version Visualization version GIF version | ||
| Description: Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.) |
| Ref | Expression |
|---|---|
| fmpt.1 | ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) |
| fmpti.2 | ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵) |
| Ref | Expression |
|---|---|
| fmpti | ⊢ 𝐹:𝐴⟶𝐵 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fmpti.2 | . . 3 ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵) | |
| 2 | 1 | rgen 3053 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 |
| 3 | fmpt.1 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) | |
| 4 | 3 | fmpt 7055 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) |
| 5 | 2, 4 | mpbi 230 | 1 ⊢ 𝐹:𝐴⟶𝐵 |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2113 ∀wral 3051 ↦ cmpt 5179 ⟶wf 6488 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pr 5377 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ral 3052 df-rex 3061 df-rab 3400 df-v 3442 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-sn 4581 df-pr 4583 df-op 4587 df-br 5099 df-opab 5161 df-mpt 5180 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-fun 6494 df-fn 6495 df-f 6496 |
| This theorem is referenced by: harf 9463 r0weon 9922 dfac2a 10040 ackbij1lem10 10138 cff 10158 isf32lem9 10271 fin1a2lem2 10311 fin1a2lem4 10313 facmapnn 14208 wwlktovf 14879 cjf 15027 ref 15035 imf 15036 absf 15261 limsupcl 15396 limsupgf 15398 eff 16004 sinf 16049 cosf 16050 bitsf 16354 fnum 16669 fden 16670 prmgapprmo 16990 setcepi 18012 catcfuccl 18042 smndex1ibas 18825 smndex2dbas 18839 smndex2hbas 18841 staffval 20774 ocvfval 21621 pjfval 21661 pjpm 21663 psdmul 22109 psdmvr 22112 leordtval2 23156 lecldbas 23163 nmfval 24532 nmoffn 24655 nmofval 24658 divcnOLD 24813 divcn 24815 xrhmeo 24900 tcphex 25173 tchnmfval 25184 ioorf 25530 dveflem 25939 tdeglem1 26019 resinf1o 26501 efifo 26512 logcnlem5 26611 resqrtcn 26715 asinf 26838 acosf 26840 atanf 26846 leibpilem2 26907 areaf 26927 emcllem1 26962 igamf 27017 chtf 27074 chpf 27089 ppif 27096 muf 27106 bposlem7 27257 2lgslem1b 27359 pntrf 27530 pntrsumo1 27532 pntsf 27540 pntrlog2bndlem4 27547 pntrlog2bndlem5 27548 oldf 27833 newf 27834 leftf 27851 rightf 27852 normf 31198 hosubcli 31844 cnlnadjlem4 32145 cnlnadjlem6 32147 zringfrac 33635 eulerpartlemsf 34516 fiblem 34555 signsvvf 34736 derangf 35362 snmlff 35523 ex-sategoelel12 35621 sinccvglem 35866 circum 35868 dnif 36674 f1omptsnlem 37541 phpreu 37805 poimirlem26 37847 cncfres 37966 lsatset 39250 clsk1independent 44287 lhe4.4ex1a 44570 absfico 45462 clim1fr1 45847 liminfgf 46002 limsup10ex 46017 liminf10ex 46018 dvsinax 46157 wallispilem5 46313 wallispi 46314 stirlinglem5 46322 stirlinglem13 46330 stirlinglem14 46331 stirlinglem15 46332 stirlingr 46334 fourierdlem43 46394 fourierdlem57 46407 fourierdlem58 46408 fourierdlem62 46412 fouriersw 46475 0ome 46773 sprsymrelf 47741 fmtnof1 47781 prmdvdsfmtnof 47832 uspgrsprf 48392 ackendofnn0 48930 |
| Copyright terms: Public domain | W3C validator |