Theorem dmmpti 6665

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

Syntax hints:   = wceq 1560   ∈ wcel 2142  Vcvv 3454   ↦ cmpt 5181  dom cdm 5647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-fun 6523  df-fn 6524

This theorem is referenced by:  fvmptex  6990  resfunexg  7199  brtpos2  8212  pwfilem  9262  inlresf  9872  inrresf  9874  sgndm  15109  vdwlem8  17024  oppccatf  17760  lubdm  18381  glbdm  18394  mndpsuppss  18799  dprd2dlem2  20082  dprd2dlem1  20083  dprd2da  20084  ablfac1c  20113  ablfac1eu  20115  ablfaclem2  20128  ablfaclem3  20129  elocv  21720  dmtopon  22983  dfac14  23678  kqtop  23805  symgtgp  24166  eltsms  24193  ressprdsds  24431  minveclem1  25486  isi1f  25736  itg1val  25745  cmvth  26053  mvth  26054  lhop2  26077  dvfsumabs  26085  dvfsumrlim2  26094  taylthlem1  26436  taylthlem2  26437  ulmdvlem1  26463  pige3ALT  26585  relogcn  26703  atandm  26941  atanf  26945  atancn  27001  dmarea  27022  dfarea  27025  efrlim  27034  lgamgulmlem2  27094  dchrptlem2  27329  dchrptlem3  27330  dchrisum0  27584  nosupno  27767  nosupdm  27768  nosupbday  27769  nosupres  27771  nosupbnd1lem1  27772  noinfno  27782  noinfdm  27783  incistruhgr  29280  vsfval  30836  ipasslem8  31040  minvecolem1  31077  xppreima2  32853  ofpreima  32867  rmfsupp2  33418  zarclsint  34169  zartopn  34172  zarmxt1  34177  zarcmplem  34178  dmsigagen  34441  measbase  34494  sseqf  34689  ballotlem7  34833  bj-inftyexpitaudisj  37697  bj-inftyexpidisj  37702  bj-elccinfty  37706  bj-minftyccb  37717  fin2so  38106  poimirlem30  38149  poimir  38152  dvtan  38169  itg2addnclem2  38171  ftc1anclem6  38197  totbndbnd  38288  tfsconcatrev  43925  comptiunov2i  44282  lhe4.4ex1a  44905  dvsinax  46487  fourierdlem62  46742  fourierdlem70  46750  fourierdlem71  46751  fourierdlem80  46760  fouriersw  46805  smflimsuplem1  47394  smflimsuplem4  47397  scmsuppss  48993  lincext2  49077  idfurcl  49719  reldmprcof1  50002  reldmlmd2  50274  reldmcmd2  50275  aacllem  50422