Theorem dmmpti 6695

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

Syntax hints:   = wceq 1539   ∈ wcel 2104  Vcvv 3472   ↦ cmpt 5232  dom cdm 5677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-fun 6546  df-fn 6547

This theorem is referenced by:  fvmptex  7013  resfunexg  7220  brtpos2  8221  pwfilem  9181  inlresf  9913  inrresf  9915  vdwlem8  16927  oppccatf  17680  lubdm  18310  glbdm  18323  dprd2dlem2  19953  dprd2dlem1  19954  dprd2da  19955  ablfac1c  19984  ablfac1eu  19986  ablfaclem2  19999  ablfaclem3  20000  elocv  21442  dmtopon  22647  dfac14  23344  kqtop  23471  symgtgp  23832  eltsms  23859  ressprdsds  24099  minveclem1  25174  isi1f  25425  itg1val  25434  cmvth  25742  mvth  25743  lhop2  25766  dvfsumabs  25774  dvfsumrlim2  25783  taylthlem1  26119  taylthlem2  26120  ulmdvlem1  26146  pige3ALT  26263  relogcn  26380  atandm  26615  atanf  26619  atancn  26675  dmarea  26696  dfarea  26699  efrlim  26708  lgamgulmlem2  26768  dchrptlem2  27002  dchrptlem3  27003  dchrisum0  27257  nosupno  27440  nosupdm  27441  nosupbday  27442  nosupres  27444  nosupbnd1lem1  27445  noinfno  27455  noinfdm  27456  incistruhgr  28604  vsfval  30151  ipasslem8  30355  minvecolem1  30392  xppreima2  32141  ofpreima  32155  rmfsupp2  32655  zarclsint  33148  zartopn  33151  zarmxt1  33156  zarcmplem  33157  dmsigagen  33438  measbase  33491  sseqf  33687  ballotlem7  33830  gg-cmvth  35469  bj-inftyexpitaudisj  36391  bj-inftyexpidisj  36396  bj-elccinfty  36400  bj-minftyccb  36411  fin2so  36780  poimirlem30  36823  poimir  36826  dvtan  36843  itg2addnclem2  36845  ftc1anclem6  36871  totbndbnd  36962  tfsconcatrev  42402  comptiunov2i  42761  lhe4.4ex1a  43392  dvsinax  44929  fourierdlem62  45184  fourierdlem70  45192  fourierdlem71  45193  fourierdlem80  45202  fouriersw  45247  smflimsuplem1  45836  smflimsuplem4  45839  mndpsuppss  47137  scmsuppss  47138  lincext2  47225  aacllem  47937