![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dmmpti | Structured version Visualization version GIF version |
Description: Domain of the mapping operation. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Ref | Expression |
---|---|
fnmpti.1 | ⊢ 𝐵 ∈ V |
fnmpti.2 | ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
Ref | Expression |
---|---|
dmmpti | ⊢ dom 𝐹 = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnmpti.1 | . . 3 ⊢ 𝐵 ∈ V | |
2 | fnmpti.2 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
3 | 1, 2 | fnmpti 6699 | . 2 ⊢ 𝐹 Fn 𝐴 |
4 | 3 | fndmi 6659 | 1 ⊢ dom 𝐹 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 ∈ wcel 2098 Vcvv 3461 ↦ cmpt 5232 dom cdm 5678 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-fun 6551 df-fn 6552 |
This theorem is referenced by: fvmptex 7018 resfunexg 7227 brtpos2 8238 pwfilem 9202 inlresf 9939 inrresf 9941 vdwlem8 16960 oppccatf 17713 lubdm 18346 glbdm 18359 dprd2dlem2 20009 dprd2dlem1 20010 dprd2da 20011 ablfac1c 20040 ablfac1eu 20042 ablfaclem2 20055 ablfaclem3 20056 elocv 21617 dmtopon 22869 dfac14 23566 kqtop 23693 symgtgp 24054 eltsms 24081 ressprdsds 24321 minveclem1 25396 isi1f 25647 itg1val 25656 cmvth 25967 cmvthOLD 25968 mvth 25969 lhop2 25992 dvfsumabs 26001 dvfsumrlim2 26011 taylthlem1 26353 taylthlem2 26354 taylthlem2OLD 26355 ulmdvlem1 26381 pige3ALT 26499 relogcn 26617 atandm 26853 atanf 26857 atancn 26913 dmarea 26934 dfarea 26937 efrlim 26946 efrlimOLD 26947 lgamgulmlem2 27007 dchrptlem2 27243 dchrptlem3 27244 dchrisum0 27498 nosupno 27682 nosupdm 27683 nosupbday 27684 nosupres 27686 nosupbnd1lem1 27687 noinfno 27697 noinfdm 27698 incistruhgr 28964 vsfval 30515 ipasslem8 30719 minvecolem1 30756 xppreima2 32518 ofpreima 32532 rmfsupp2 33038 zarclsint 33601 zartopn 33604 zarmxt1 33609 zarcmplem 33610 dmsigagen 33891 measbase 33944 sseqf 34140 ballotlem7 34283 bj-inftyexpitaudisj 36812 bj-inftyexpidisj 36817 bj-elccinfty 36821 bj-minftyccb 36832 fin2so 37208 poimirlem30 37251 poimir 37254 dvtan 37271 itg2addnclem2 37273 ftc1anclem6 37299 totbndbnd 37390 tfsconcatrev 42916 comptiunov2i 43275 lhe4.4ex1a 43905 dvsinax 45436 fourierdlem62 45691 fourierdlem70 45699 fourierdlem71 45700 fourierdlem80 45709 fouriersw 45754 smflimsuplem1 46343 smflimsuplem4 46346 mndpsuppss 47618 scmsuppss 47619 lincext2 47706 aacllem 48417 |
Copyright terms: Public domain | W3C validator |