Theorem dmmpti 6200

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 6199	. 2 ⊢ 𝐹 Fn 𝐴
4		fndm 6167	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
5	3, 4	ax-mp 5	1 ⊢ dom 𝐹 = 𝐴

Syntax hints:   = wceq 1652   ∈ wcel 2155  Vcvv 3349   ↦ cmpt 4887  dom cdm 5276   Fn wfn 6062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940  ax-nul 4948  ax-pr 5061

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ral 3059  df-rab 3063  df-v 3351  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-sn 4334  df-pr 4336  df-op 4340  df-br 4809  df-opab 4871  df-mpt 4888  df-id 5184  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-fun 6069  df-fn 6070

This theorem is referenced by:  fvmptex  6482  resfunexg  6671  brtpos2  7560  inlresf  8990  inrresf  8992  vdwlem8  15972  lubdm  17246  glbdm  17259  dprd2dlem2  18705  dprd2dlem1  18706  dprd2da  18707  ablfac1c  18736  ablfac1eu  18738  ablfaclem2  18751  ablfaclem3  18752  elocv  20287  dmtopon  21006  dfac14  21700  kqtop  21827  symgtgp  22183  eltsms  22214  ressprdsds  22454  minveclem1  23483  isi1f  23731  itg1val  23740  cmvth  24044  mvth  24045  lhop2  24068  dvfsumabs  24076  dvfsumrlim2  24085  taylthlem1  24417  taylthlem2  24418  ulmdvlem1  24444  pige3  24560  relogcn  24674  atandm  24893  atanf  24897  atancn  24953  dmarea  24974  dfarea  24977  efrlim  24986  lgamgulmlem2  25046  dchrptlem2  25280  dchrptlem3  25281  dchrisum0  25499  eleenn  26066  incistruhgr  26250  vsfval  27878  ipasslem8  28082  minvecolem1  28120  xppreima2  29834  ofpreima  29849  dmsigagen  30588  measbase  30641  sseqf  30836  ballotlem7  30979  nosupno  32224  nosupdm  32225  nosupbday  32226  nosupres  32228  nosupbnd1lem1  32229  bj-inftyexpidisj  33463  bj-elccinfty  33467  bj-minftyccb  33478  fin2so  33752  poimirlem30  33795  poimir  33798  dvtan  33815  itg2addnclem2  33817  ftc1anclem6  33845  totbndbnd  33942  comptiunov2i  38605  lhe4.4ex1a  39134  dvsinax  40697  fourierdlem62  40954  fourierdlem70  40962  fourierdlem71  40963  fourierdlem80  40972  fouriersw  41017  smflimsuplem1  41598  smflimsuplem4  41601  mndpsuppss  42753  scmsuppss  42754  lincext2  42845  aacllem  43151