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 2906 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 |
3 | fmpt.1 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) | |
4 | 3 | fmpt 6289 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) |
5 | 2, 4 | mpbi 219 | 1 ⊢ 𝐹:𝐴⟶𝐵 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∈ wcel 1977 ∀wral 2896 ↦ cmpt 4643 ⟶wf 5800 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-sbc 3403 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-fv 5812 |
This theorem is referenced by: harf 8348 r0weon 8718 dfac2a 8835 ackbij1lem10 8934 cff 8953 isf32lem9 9066 fin1a2lem2 9106 fin1a2lem4 9108 facmapnn 12934 wwlktovf 13547 cjf 13692 ref 13700 imf 13701 absf 13925 limsupcl 14052 limsupgf 14054 eff 14651 sinf 14693 cosf 14694 bitsf 14987 fnum 15288 fden 15289 prmgapprmo 15604 setcepi 16561 catcfuccl 16582 staffval 18670 ocvfval 19829 pjfval 19869 pjpm 19871 leordtval2 20826 lecldbas 20833 nmfval 22203 nmoffn 22325 nmofval 22328 divcn 22479 xrhmeo 22553 tchex 22824 tchnmfval 22835 ioorf 23147 dveflem 23546 resinf1o 24086 efifo 24097 logcnlem5 24192 resqrtcn 24290 asinf 24399 acosf 24401 atanf 24407 leibpilem2 24468 areaf 24488 emcllem1 24522 igamf 24577 chtf 24634 chpf 24649 ppif 24656 muf 24666 bposlem7 24815 2lgslem1b 24917 pntrf 25052 pntrsumo1 25054 pntsf 25062 pntrlog2bndlem4 25069 pntrlog2bndlem5 25070 normf 27364 hosubcli 28012 cnlnadjlem4 28313 cnlnadjlem6 28315 eulerpartlemsf 29748 fiblem 29787 signsvvf 29982 derangf 30404 snmlff 30565 sinccvglem 30820 circum 30822 dnif 31634 f1omptsnlem 32359 phpreu 32563 poimirlem26 32605 cncfres 32734 lsatset 33295 clsk1independent 37364 lhe4.4ex1a 37550 absfico 38405 clim1fr1 38668 dvsinax 38801 wallispilem5 38962 wallispi 38963 stirlinglem5 38971 stirlinglem13 38979 stirlinglem14 38980 stirlinglem15 38981 stirlingr 38983 fourierdlem43 39043 fourierdlem57 39056 fourierdlem58 39057 fourierdlem62 39061 fouriersw 39124 0ome 39419 fmtnof1 39985 prmdvdsfmtnof 40036 |
Copyright terms: Public domain | W3C validator |