Theorem dmmpti 6700

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

Syntax hints:   = wceq 1533   ∈ wcel 2098  Vcvv 3461   ↦ cmpt 5232  dom cdm 5678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-fun 6551  df-fn 6552

This theorem is referenced by:  fvmptex  7018  resfunexg  7227  brtpos2  8238  pwfilem  9202  inlresf  9939  inrresf  9941  vdwlem8  16960  oppccatf  17713  lubdm  18346  glbdm  18359  dprd2dlem2  20009  dprd2dlem1  20010  dprd2da  20011  ablfac1c  20040  ablfac1eu  20042  ablfaclem2  20055  ablfaclem3  20056  elocv  21617  dmtopon  22869  dfac14  23566  kqtop  23693  symgtgp  24054  eltsms  24081  ressprdsds  24321  minveclem1  25396  isi1f  25647  itg1val  25656  cmvth  25967  cmvthOLD  25968  mvth  25969  lhop2  25992  dvfsumabs  26001  dvfsumrlim2  26011  taylthlem1  26353  taylthlem2  26354  taylthlem2OLD  26355  ulmdvlem1  26381  pige3ALT  26499  relogcn  26617  atandm  26853  atanf  26857  atancn  26913  dmarea  26934  dfarea  26937  efrlim  26946  efrlimOLD  26947  lgamgulmlem2  27007  dchrptlem2  27243  dchrptlem3  27244  dchrisum0  27498  nosupno  27682  nosupdm  27683  nosupbday  27684  nosupres  27686  nosupbnd1lem1  27687  noinfno  27697  noinfdm  27698  incistruhgr  28964  vsfval  30515  ipasslem8  30719  minvecolem1  30756  xppreima2  32518  ofpreima  32532  rmfsupp2  33038  zarclsint  33601  zartopn  33604  zarmxt1  33609  zarcmplem  33610  dmsigagen  33891  measbase  33944  sseqf  34140  ballotlem7  34283  bj-inftyexpitaudisj  36812  bj-inftyexpidisj  36817  bj-elccinfty  36821  bj-minftyccb  36832  fin2so  37208  poimirlem30  37251  poimir  37254  dvtan  37271  itg2addnclem2  37273  ftc1anclem6  37299  totbndbnd  37390  tfsconcatrev  42916  comptiunov2i  43275  lhe4.4ex1a  43905  dvsinax  45436  fourierdlem62  45691  fourierdlem70  45699  fourierdlem71  45700  fourierdlem80  45709  fouriersw  45754  smflimsuplem1  46343  smflimsuplem4  46346  mndpsuppss  47618  scmsuppss  47619  lincext2  47706  aacllem  48417