Theorem dmmpti 6586

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

Syntax hints:   = wceq 1539   ∈ wcel 2107  Vcvv 3433   ↦ cmpt 5158  dom cdm 5590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-fun 6439  df-fn 6440

This theorem is referenced by:  fvmptex  6898  resfunexg  7100  brtpos2  8057  pwfilem  8969  inlresf  9681  inrresf  9683  vdwlem8  16698  oppccatf  17448  lubdm  18078  glbdm  18091  dprd2dlem2  19652  dprd2dlem1  19653  dprd2da  19654  ablfac1c  19683  ablfac1eu  19685  ablfaclem2  19698  ablfaclem3  19699  elocv  20882  dmtopon  22081  dfac14  22778  kqtop  22905  symgtgp  23266  eltsms  23293  ressprdsds  23533  minveclem1  24597  isi1f  24847  itg1val  24856  cmvth  25164  mvth  25165  lhop2  25188  dvfsumabs  25196  dvfsumrlim2  25205  taylthlem1  25541  taylthlem2  25542  ulmdvlem1  25568  pige3ALT  25685  relogcn  25802  atandm  26035  atanf  26039  atancn  26095  dmarea  26116  dfarea  26119  efrlim  26128  lgamgulmlem2  26188  dchrptlem2  26422  dchrptlem3  26423  dchrisum0  26677  incistruhgr  27458  vsfval  29004  ipasslem8  29208  minvecolem1  29245  xppreima2  30997  ofpreima  31011  rmfsupp2  31501  zarclsint  31831  zartopn  31834  zarmxt1  31839  zarcmplem  31840  dmsigagen  32121  measbase  32174  sseqf  32368  ballotlem7  32511  nosupno  33915  nosupdm  33916  nosupbday  33917  nosupres  33919  nosupbnd1lem1  33920  noinfno  33930  noinfdm  33931  bj-inftyexpitaudisj  35385  bj-inftyexpidisj  35390  bj-elccinfty  35394  bj-minftyccb  35405  fin2so  35773  poimirlem30  35816  poimir  35819  dvtan  35836  itg2addnclem2  35838  ftc1anclem6  35864  totbndbnd  35956  comptiunov2i  41321  lhe4.4ex1a  41954  dvsinax  43461  fourierdlem62  43716  fourierdlem70  43724  fourierdlem71  43725  fourierdlem80  43734  fouriersw  43779  smflimsuplem1  44364  smflimsuplem4  44367  mndpsuppss  45718  scmsuppss  45719  lincext2  45807  aacllem  46516