![]() |
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 3062 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 |
3 | fmpt.1 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) | |
4 | 3 | fmpt 7094 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) |
5 | 2, 4 | mpbi 229 | 1 ⊢ 𝐹:𝐴⟶𝐵 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2106 ∀wral 3060 ↦ cmpt 5224 ⟶wf 6528 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5292 ax-nul 5299 ax-pr 5420 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4523 df-sn 4623 df-pr 4625 df-op 4629 df-br 5142 df-opab 5204 df-mpt 5225 df-id 5567 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-fun 6534 df-fn 6535 df-f 6536 |
This theorem is referenced by: harf 9535 r0weon 9989 dfac2a 10106 ackbij1lem10 10206 cff 10225 isf32lem9 10338 fin1a2lem2 10378 fin1a2lem4 10380 facmapnn 14227 wwlktovf 14889 cjf 15033 ref 15041 imf 15042 absf 15266 limsupcl 15399 limsupgf 15401 eff 16007 sinf 16049 cosf 16050 bitsf 16350 fnum 16660 fden 16661 prmgapprmo 16977 setcepi 18020 catcfuccl 18051 catcfucclOLD 18052 smndex1ibas 18756 smndex2dbas 18770 smndex2hbas 18772 staffval 20404 ocvfval 21152 pjfval 21194 pjpm 21196 leordtval2 22645 lecldbas 22652 nmfval 24026 nmoffn 24157 nmofval 24160 divcn 24313 xrhmeo 24391 tcphex 24663 tchnmfval 24674 ioorf 25019 dveflem 25425 tdeglem1 25502 resinf1o 25974 efifo 25985 logcnlem5 26083 resqrtcn 26184 asinf 26304 acosf 26306 atanf 26312 leibpilem2 26373 areaf 26393 emcllem1 26427 igamf 26482 chtf 26539 chpf 26554 ppif 26561 muf 26571 bposlem7 26720 2lgslem1b 26822 pntrf 26993 pntrsumo1 26995 pntsf 27003 pntrlog2bndlem4 27010 pntrlog2bndlem5 27011 oldf 27275 newf 27276 leftf 27283 rightf 27284 normf 30239 hosubcli 30885 cnlnadjlem4 31186 cnlnadjlem6 31188 eulerpartlemsf 33189 fiblem 33228 signsvvf 33421 derangf 33990 snmlff 34151 ex-sategoelel12 34249 sinccvglem 34488 circum 34490 dnif 35154 f1omptsnlem 36021 phpreu 36276 poimirlem26 36318 cncfres 36438 lsatset 37665 clsk1independent 42568 lhe4.4ex1a 42859 absfico 43688 clim1fr1 44090 liminfgf 44247 limsup10ex 44262 liminf10ex 44263 dvsinax 44402 wallispilem5 44558 wallispi 44559 stirlinglem5 44567 stirlinglem13 44575 stirlinglem14 44576 stirlinglem15 44577 stirlingr 44579 fourierdlem43 44639 fourierdlem57 44652 fourierdlem58 44653 fourierdlem62 44657 fouriersw 44720 0ome 45018 sprsymrelf 45935 fmtnof1 45975 prmdvdsfmtnof 46026 uspgrsprf 46296 ackendofnn0 47018 |
Copyright terms: Public domain | W3C validator |