Theorem dmmpti 6712

Description: Domain of the mapping operation. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 31-Aug-2015.)

Hypotheses

Ref	Expression
fnmpti.1	⊢ 𝐵 ∈ V
fnmpti.2	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

Assertion

Ref	Expression
dmmpti	⊢ dom 𝐹 = 𝐴

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem dmmpti

Step	Hyp	Ref	Expression
1		fnmpti.1	. . 3 ⊢ 𝐵 ∈ V
2		fnmpti.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	1, 2	fnmpti 6711	. 2 ⊢ 𝐹 Fn 𝐴
4	3	fndmi 6672	1 ⊢ dom 𝐹 = 𝐴

Syntax hints:   = wceq 1536   ∈ wcel 2105  Vcvv 3477   ↦ cmpt 5230  dom cdm 5688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-fun 6564  df-fn 6565

This theorem is referenced by:  fvmptex  7029  resfunexg  7234  brtpos2  8255  pwfilem  9353  inlresf  9951  inrresf  9953  vdwlem8  17021  oppccatf  17774  lubdm  18408  glbdm  18421  mndpsuppss  18790  dprd2dlem2  20074  dprd2dlem1  20075  dprd2da  20076  ablfac1c  20105  ablfac1eu  20107  ablfaclem2  20120  ablfaclem3  20121  elocv  21703  dmtopon  22944  dfac14  23641  kqtop  23768  symgtgp  24129  eltsms  24156  ressprdsds  24396  minveclem1  25471  isi1f  25722  itg1val  25731  cmvth  26043  cmvthOLD  26044  mvth  26045  lhop2  26068  dvfsumabs  26077  dvfsumrlim2  26087  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  ulmdvlem1  26457  pige3ALT  26576  relogcn  26694  atandm  26933  atanf  26937  atancn  26993  dmarea  27014  dfarea  27017  efrlim  27026  efrlimOLD  27027  lgamgulmlem2  27087  dchrptlem2  27323  dchrptlem3  27324  dchrisum0  27578  nosupno  27762  nosupdm  27763  nosupbday  27764  nosupres  27766  nosupbnd1lem1  27767  noinfno  27777  noinfdm  27778  incistruhgr  29110  vsfval  30661  ipasslem8  30865  minvecolem1  30902  xppreima2  32667  ofpreima  32681  rmfsupp2  33227  zarclsint  33832  zartopn  33835  zarmxt1  33840  zarcmplem  33841  dmsigagen  34124  measbase  34177  sseqf  34373  ballotlem7  34516  bj-inftyexpitaudisj  37187  bj-inftyexpidisj  37192  bj-elccinfty  37196  bj-minftyccb  37207  fin2so  37593  poimirlem30  37636  poimir  37639  dvtan  37656  itg2addnclem2  37658  ftc1anclem6  37684  totbndbnd  37775  tfsconcatrev  43337  comptiunov2i  43695  lhe4.4ex1a  44324  dvsinax  45868  fourierdlem62  46123  fourierdlem70  46131  fourierdlem71  46132  fourierdlem80  46141  fouriersw  46186  smflimsuplem1  46775  smflimsuplem4  46778  scmsuppss  48215  lincext2  48300  aacllem  49031