| 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 3063 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 |
| 3 | fmpt.1 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) | |
| 4 | 3 | fmpt 7130 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) |
| 5 | 2, 4 | mpbi 230 | 1 ⊢ 𝐹:𝐴⟶𝐵 |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 ∀wral 3061 ↦ cmpt 5225 ⟶wf 6557 |
| 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-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 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-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-fun 6563 df-fn 6564 df-f 6565 |
| This theorem is referenced by: harf 9598 r0weon 10052 dfac2a 10170 ackbij1lem10 10268 cff 10288 isf32lem9 10401 fin1a2lem2 10441 fin1a2lem4 10443 facmapnn 14324 wwlktovf 14995 cjf 15143 ref 15151 imf 15152 absf 15376 limsupcl 15509 limsupgf 15511 eff 16117 sinf 16160 cosf 16161 bitsf 16464 fnum 16779 fden 16780 prmgapprmo 17100 setcepi 18133 catcfuccl 18163 smndex1ibas 18913 smndex2dbas 18927 smndex2hbas 18929 staffval 20842 ocvfval 21684 pjfval 21726 pjpm 21728 psdmul 22170 psdmvr 22173 leordtval2 23220 lecldbas 23227 nmfval 24601 nmoffn 24732 nmofval 24735 divcnOLD 24890 divcn 24892 xrhmeo 24977 tcphex 25251 tchnmfval 25262 ioorf 25608 dveflem 26017 tdeglem1 26097 resinf1o 26578 efifo 26589 logcnlem5 26688 resqrtcn 26792 asinf 26915 acosf 26917 atanf 26923 leibpilem2 26984 areaf 27004 emcllem1 27039 igamf 27094 chtf 27151 chpf 27166 ppif 27173 muf 27183 bposlem7 27334 2lgslem1b 27436 pntrf 27607 pntrsumo1 27609 pntsf 27617 pntrlog2bndlem4 27624 pntrlog2bndlem5 27625 oldf 27896 newf 27897 leftf 27904 rightf 27905 normf 31142 hosubcli 31788 cnlnadjlem4 32089 cnlnadjlem6 32091 zringfrac 33582 eulerpartlemsf 34361 fiblem 34400 signsvvf 34594 derangf 35173 snmlff 35334 ex-sategoelel12 35432 sinccvglem 35677 circum 35679 dnif 36475 f1omptsnlem 37337 phpreu 37611 poimirlem26 37653 cncfres 37772 lsatset 38991 clsk1independent 44059 lhe4.4ex1a 44348 absfico 45223 clim1fr1 45616 liminfgf 45773 limsup10ex 45788 liminf10ex 45789 dvsinax 45928 wallispilem5 46084 wallispi 46085 stirlinglem5 46093 stirlinglem13 46101 stirlinglem14 46102 stirlinglem15 46103 stirlingr 46105 fourierdlem43 46165 fourierdlem57 46178 fourierdlem58 46179 fourierdlem62 46183 fouriersw 46246 0ome 46544 sprsymrelf 47482 fmtnof1 47522 prmdvdsfmtnof 47573 uspgrsprf 48062 ackendofnn0 48605 |
| Copyright terms: Public domain | W3C validator |