Theorem dmmpti 6561

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 6560	. 2 ⊢ 𝐹 Fn 𝐴
4	3	fndmi 6521	1 ⊢ dom 𝐹 = 𝐴

Syntax hints:   = wceq 1539   ∈ wcel 2108  Vcvv 3422   ↦ cmpt 5153  dom cdm 5580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-fun 6420  df-fn 6421

This theorem is referenced by:  fvmptex  6871  resfunexg  7073  brtpos2  8019  pwfilem  8922  inlresf  9603  inrresf  9605  vdwlem8  16617  oppccatf  17356  lubdm  17984  glbdm  17997  dprd2dlem2  19558  dprd2dlem1  19559  dprd2da  19560  ablfac1c  19589  ablfac1eu  19591  ablfaclem2  19604  ablfaclem3  19605  elocv  20785  dmtopon  21980  dfac14  22677  kqtop  22804  symgtgp  23165  eltsms  23192  ressprdsds  23432  minveclem1  24493  isi1f  24743  itg1val  24752  cmvth  25060  mvth  25061  lhop2  25084  dvfsumabs  25092  dvfsumrlim2  25101  taylthlem1  25437  taylthlem2  25438  ulmdvlem1  25464  pige3ALT  25581  relogcn  25698  atandm  25931  atanf  25935  atancn  25991  dmarea  26012  dfarea  26015  efrlim  26024  lgamgulmlem2  26084  dchrptlem2  26318  dchrptlem3  26319  dchrisum0  26573  incistruhgr  27352  vsfval  28896  ipasslem8  29100  minvecolem1  29137  xppreima2  30889  ofpreima  30904  rmfsupp2  31394  zarclsint  31724  zartopn  31727  zarmxt1  31732  zarcmplem  31733  dmsigagen  32012  measbase  32065  sseqf  32259  ballotlem7  32402  nosupno  33833  nosupdm  33834  nosupbday  33835  nosupres  33837  nosupbnd1lem1  33838  noinfno  33848  noinfdm  33849  bj-inftyexpitaudisj  35303  bj-inftyexpidisj  35308  bj-elccinfty  35312  bj-minftyccb  35323  fin2so  35691  poimirlem30  35734  poimir  35737  dvtan  35754  itg2addnclem2  35756  ftc1anclem6  35782  totbndbnd  35874  comptiunov2i  41203  lhe4.4ex1a  41836  dvsinax  43344  fourierdlem62  43599  fourierdlem70  43607  fourierdlem71  43608  fourierdlem80  43617  fouriersw  43662  smflimsuplem1  44240  smflimsuplem4  44243  mndpsuppss  45595  scmsuppss  45596  lincext2  45684  aacllem  46391