![]() |
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 6259 | . 2 ⊢ 𝐹 Fn 𝐴 |
4 | fndm 6227 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
5 | 3, 4 | ax-mp 5 | 1 ⊢ dom 𝐹 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1656 ∈ wcel 2164 Vcvv 3414 ↦ cmpt 4954 dom cdm 5346 Fn wfn 6122 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 ax-sep 5007 ax-nul 5015 ax-pr 5129 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ral 3122 df-rab 3126 df-v 3416 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4147 df-if 4309 df-sn 4400 df-pr 4402 df-op 4406 df-br 4876 df-opab 4938 df-mpt 4955 df-id 5252 df-xp 5352 df-rel 5353 df-cnv 5354 df-co 5355 df-dm 5356 df-fun 6129 df-fn 6130 |
This theorem is referenced by: fvmptex 6546 resfunexg 6740 brtpos2 7628 inlresf 9060 inrresf 9062 vdwlem8 16070 lubdm 17339 glbdm 17352 dprd2dlem2 18800 dprd2dlem1 18801 dprd2da 18802 ablfac1c 18831 ablfac1eu 18833 ablfaclem2 18846 ablfaclem3 18847 elocv 20382 dmtopon 21105 dfac14 21799 kqtop 21926 symgtgp 22282 eltsms 22313 ressprdsds 22553 minveclem1 23599 isi1f 23847 itg1val 23856 cmvth 24160 mvth 24161 lhop2 24184 dvfsumabs 24192 dvfsumrlim2 24201 taylthlem1 24533 taylthlem2 24534 ulmdvlem1 24560 pige3 24676 relogcn 24790 atandm 25023 atanf 25027 atancn 25083 dmarea 25104 dfarea 25107 efrlim 25116 lgamgulmlem2 25176 dchrptlem2 25410 dchrptlem3 25411 dchrisum0 25629 eleenn 26202 incistruhgr 26384 vsfval 28039 ipasslem8 28243 minvecolem1 28281 xppreima2 29995 ofpreima 30010 dmsigagen 30748 measbase 30801 sseqf 30996 ballotlem7 31139 nosupno 32383 nosupdm 32384 nosupbday 32385 nosupres 32387 nosupbnd1lem1 32388 bj-inftyexpitaudisj 33627 bj-inftyexpidisj 33632 bj-elccinfty 33636 bj-minftyccb 33647 fin2so 33934 poimirlem30 33978 poimir 33981 dvtan 33998 itg2addnclem2 34000 ftc1anclem6 34028 totbndbnd 34125 comptiunov2i 38834 lhe4.4ex1a 39363 dvsinax 40916 fourierdlem62 41173 fourierdlem70 41181 fourierdlem71 41182 fourierdlem80 41191 fouriersw 41236 smflimsuplem1 41814 smflimsuplem4 41817 mndpsuppss 43013 scmsuppss 43014 lincext2 43105 aacllem 43453 |
Copyright terms: Public domain | W3C validator |