| 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 6682 | . 2 ⊢ 𝐹 Fn 𝐴 |
| 4 | 3 | fndmi 6643 | 1 ⊢ dom 𝐹 = 𝐴 |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: = wceq 1570 ∈ wcel 2146 Vcvv 3457 ↦ cmpt 5194 dom cdm 5663 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-sep 5259 ax-pr 5406 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ral 3082 df-rex 3092 df-rab 3419 df-v 3459 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-sn 4592 df-pr 4594 df-op 4598 df-br 5112 df-opab 5176 df-mpt 5195 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-fun 6542 df-fn 6543 |
| This theorem is used by: fvmptex 7008 resfunexg 7220 brtpos2 8234 pwfilem 9284 inlresf 9916 inrresf 9918 sgndm 15157 vdwlem8 17070 oppccatf 17806 lubdm 18427 glbdm 18440 mndpsuppss 18860 dprd2dlem2 20156 dprd2dlem1 20157 dprd2da 20158 ablfac1c 20187 ablfac1eu 20189 ablfaclem2 20202 ablfaclem3 20203 elocv 21868 dmtopon 23130 dfac14 23826 kqtop 23953 symgtgp 24314 eltsms 24341 ressprdsds 24579 minveclem1 25634 isi1f 25884 itg1val 25893 cmvth 26201 mvth 26202 lhop2 26225 dvfsumabs 26233 dvfsumrlim2 26242 taylthlem1 26587 taylthlem2 26588 ulmdvlem1 26614 pige3ALT 26736 relogcn 26854 atandm 27092 atanf 27096 atancn 27152 dmarea 27173 dfarea 27176 efrlim 27185 lgamgulmlem2 27245 dchrptlem2 27480 dchrptlem3 27481 dchrisum0 27735 nosupno 27918 nosupdm 27919 nosupbday 27920 nosupres 27922 nosupbnd1lem1 27923 noinfno 27933 noinfdm 27934 incistruhgr 29484 vsfval 31056 ipasslem8 31260 minvecolem1 31297 xppreima2 33067 ofpreima 33081 rmfsupp2 33621 zarclsint 34326 zartopn 34329 zarmxt1 34334 zarcmplem 34335 dmsigagen 34599 measbase 34652 sseqf 34847 ballotlem7 34991 bj-inftyexpitaudisj 37906 bj-inftyexpidisj 37911 bj-elccinfty 37915 bj-minftyccb 37926 fin2so 38315 poimirlem30 38358 poimir 38361 dvtan 38378 itg2addnclem2 38380 ftc1anclem6 38406 totbndbnd 38498 tfsconcatrev 44133 comptiunov2i 44490 lhe4.4ex1a 45097 dvsinax 46685 fourierdlem62 46940 fourierdlem70 46948 fourierdlem71 46949 fourierdlem80 46958 fouriersw 47003 smflimsuplem1 47592 smflimsuplem4 47595 scmsuppss 49208 lincext2 49292 idfurcl 49933 reldmprcof1 50216 reldmlmd2 50488 reldmcmd2 50489 aacllem 50678 |
| Copyright terms: Public domain | W3C validator |