Theorem dmmpti 6644

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  Vcvv 3442   ↦ cmpt 5181  dom cdm 5632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-fun 6502  df-fn 6503

This theorem is referenced by:  fvmptex  6964  resfunexg  7171  brtpos2  8184  pwfilem  9230  inlresf  9838  inrresf  9840  vdwlem8  16928  oppccatf  17663  lubdm  18284  glbdm  18297  mndpsuppss  18702  dprd2dlem2  19983  dprd2dlem1  19984  dprd2da  19985  ablfac1c  20014  ablfac1eu  20016  ablfaclem2  20029  ablfaclem3  20030  elocv  21635  dmtopon  22879  dfac14  23574  kqtop  23701  symgtgp  24062  eltsms  24089  ressprdsds  24327  minveclem1  25392  isi1f  25643  itg1val  25652  cmvth  25963  cmvthOLD  25964  mvth  25965  lhop2  25988  dvfsumabs  25997  dvfsumrlim2  26007  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  ulmdvlem1  26377  pige3ALT  26497  relogcn  26615  atandm  26854  atanf  26858  atancn  26914  dmarea  26935  dfarea  26938  efrlim  26947  efrlimOLD  26948  lgamgulmlem2  27008  dchrptlem2  27244  dchrptlem3  27245  dchrisum0  27499  nosupno  27683  nosupdm  27684  nosupbday  27685  nosupres  27687  nosupbnd1lem1  27688  noinfno  27698  noinfdm  27699  incistruhgr  29164  vsfval  30721  ipasslem8  30925  minvecolem1  30962  xppreima2  32741  ofpreima  32755  rmfsupp2  33332  zarclsint  34050  zartopn  34053  zarmxt1  34058  zarcmplem  34059  dmsigagen  34322  measbase  34375  sseqf  34570  ballotlem7  34714  bj-inftyexpitaudisj  37460  bj-inftyexpidisj  37465  bj-elccinfty  37469  bj-minftyccb  37480  fin2so  37858  poimirlem30  37901  poimir  37904  dvtan  37921  itg2addnclem2  37923  ftc1anclem6  37949  totbndbnd  38040  tfsconcatrev  43705  comptiunov2i  44062  lhe4.4ex1a  44685  dvsinax  46271  fourierdlem62  46526  fourierdlem70  46534  fourierdlem71  46535  fourierdlem80  46544  fouriersw  46589  smflimsuplem1  47178  smflimsuplem4  47181  scmsuppss  48731  lincext2  48815  idfurcl  49457  reldmprcof1  49740  reldmlmd2  50012  reldmcmd2  50013  aacllem  50160