Theorem dmmpti 6681

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  Vcvv 3459   ↦ cmpt 5201  dom cdm 5654

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-fun 6532  df-fn 6533

This theorem is referenced by:  fvmptex  6999  resfunexg  7206  brtpos2  8229  pwfilem  9326  inlresf  9926  inrresf  9928  vdwlem8  17006  oppccatf  17738  lubdm  18359  glbdm  18372  mndpsuppss  18741  dprd2dlem2  20021  dprd2dlem1  20022  dprd2da  20023  ablfac1c  20052  ablfac1eu  20054  ablfaclem2  20067  ablfaclem3  20068  elocv  21626  dmtopon  22859  dfac14  23554  kqtop  23681  symgtgp  24042  eltsms  24069  ressprdsds  24308  minveclem1  25374  isi1f  25625  itg1val  25634  cmvth  25945  cmvthOLD  25946  mvth  25947  lhop2  25970  dvfsumabs  25979  dvfsumrlim2  25989  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  ulmdvlem1  26359  pige3ALT  26479  relogcn  26597  atandm  26836  atanf  26840  atancn  26896  dmarea  26917  dfarea  26920  efrlim  26929  efrlimOLD  26930  lgamgulmlem2  26990  dchrptlem2  27226  dchrptlem3  27227  dchrisum0  27481  nosupno  27665  nosupdm  27666  nosupbday  27667  nosupres  27669  nosupbnd1lem1  27670  noinfno  27680  noinfdm  27681  incistruhgr  29004  vsfval  30560  ipasslem8  30764  minvecolem1  30801  xppreima2  32575  ofpreima  32589  rmfsupp2  33179  zarclsint  33849  zartopn  33852  zarmxt1  33857  zarcmplem  33858  dmsigagen  34121  measbase  34174  sseqf  34370  ballotlem7  34514  bj-inftyexpitaudisj  37169  bj-inftyexpidisj  37174  bj-elccinfty  37178  bj-minftyccb  37189  fin2so  37577  poimirlem30  37620  poimir  37623  dvtan  37640  itg2addnclem2  37642  ftc1anclem6  37668  totbndbnd  37759  tfsconcatrev  43319  comptiunov2i  43677  lhe4.4ex1a  44301  dvsinax  45890  fourierdlem62  46145  fourierdlem70  46153  fourierdlem71  46154  fourierdlem80  46163  fouriersw  46208  smflimsuplem1  46797  smflimsuplem4  46800  scmsuppss  48294  lincext2  48379  idfurcl  49006  reldmprcof1  49239  reldmlmd2  49473  reldmcmd2  49474  aacllem  49613