![]() |
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 3064 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 |
3 | fmpt.1 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) | |
4 | 3 | fmpt 7110 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) |
5 | 2, 4 | mpbi 229 | 1 ⊢ 𝐹:𝐴⟶𝐵 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2107 ∀wral 3062 ↦ cmpt 5232 ⟶wf 6540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-fun 6546 df-fn 6547 df-f 6548 |
This theorem is referenced by: harf 9553 r0weon 10007 dfac2a 10124 ackbij1lem10 10224 cff 10243 isf32lem9 10356 fin1a2lem2 10396 fin1a2lem4 10398 facmapnn 14245 wwlktovf 14907 cjf 15051 ref 15059 imf 15060 absf 15284 limsupcl 15417 limsupgf 15419 eff 16025 sinf 16067 cosf 16068 bitsf 16368 fnum 16678 fden 16679 prmgapprmo 16995 setcepi 18038 catcfuccl 18069 catcfucclOLD 18070 smndex1ibas 18781 smndex2dbas 18795 smndex2hbas 18797 staffval 20455 ocvfval 21219 pjfval 21261 pjpm 21263 leordtval2 22716 lecldbas 22723 nmfval 24097 nmoffn 24228 nmofval 24231 divcn 24384 xrhmeo 24462 tcphex 24734 tchnmfval 24745 ioorf 25090 dveflem 25496 tdeglem1 25573 resinf1o 26045 efifo 26056 logcnlem5 26154 resqrtcn 26257 asinf 26377 acosf 26379 atanf 26385 leibpilem2 26446 areaf 26466 emcllem1 26500 igamf 26555 chtf 26612 chpf 26627 ppif 26634 muf 26644 bposlem7 26793 2lgslem1b 26895 pntrf 27066 pntrsumo1 27068 pntsf 27076 pntrlog2bndlem4 27083 pntrlog2bndlem5 27084 oldf 27352 newf 27353 leftf 27360 rightf 27361 normf 30376 hosubcli 31022 cnlnadjlem4 31323 cnlnadjlem6 31325 eulerpartlemsf 33358 fiblem 33397 signsvvf 33590 derangf 34159 snmlff 34320 ex-sategoelel12 34418 sinccvglem 34657 circum 34659 gg-divcn 35163 dnif 35350 f1omptsnlem 36217 phpreu 36472 poimirlem26 36514 cncfres 36633 lsatset 37860 clsk1independent 42797 lhe4.4ex1a 43088 absfico 43917 clim1fr1 44317 liminfgf 44474 limsup10ex 44489 liminf10ex 44490 dvsinax 44629 wallispilem5 44785 wallispi 44786 stirlinglem5 44794 stirlinglem13 44802 stirlinglem14 44803 stirlinglem15 44804 stirlingr 44806 fourierdlem43 44866 fourierdlem57 44879 fourierdlem58 44880 fourierdlem62 44884 fouriersw 44947 0ome 45245 sprsymrelf 46163 fmtnof1 46203 prmdvdsfmtnof 46254 uspgrsprf 46524 ackendofnn0 47370 |
Copyright terms: Public domain | W3C validator |