Theorem dmmpti 6464

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

Syntax hints:   = wceq 1538   ∈ wcel 2111  Vcvv 3441   ↦ cmpt 5110  dom cdm 5519

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-fun 6326  df-fn 6327

This theorem is referenced by:  fvmptex  6759  resfunexg  6955  brtpos2  7881  inlresf  9327  inrresf  9329  vdwlem8  16314  lubdm  17581  glbdm  17594  dprd2dlem2  19155  dprd2dlem1  19156  dprd2da  19157  ablfac1c  19186  ablfac1eu  19188  ablfaclem2  19201  ablfaclem3  19202  elocv  20357  dmtopon  21528  dfac14  22223  kqtop  22350  symgtgp  22711  eltsms  22738  ressprdsds  22978  minveclem1  24028  isi1f  24278  itg1val  24287  cmvth  24594  mvth  24595  lhop2  24618  dvfsumabs  24626  dvfsumrlim2  24635  taylthlem1  24968  taylthlem2  24969  ulmdvlem1  24995  pige3ALT  25112  relogcn  25229  atandm  25462  atanf  25466  atancn  25522  dmarea  25543  dfarea  25546  efrlim  25555  lgamgulmlem2  25615  dchrptlem2  25849  dchrptlem3  25850  dchrisum0  26104  incistruhgr  26872  vsfval  28416  ipasslem8  28620  minvecolem1  28657  xppreima2  30413  ofpreima  30428  rmfsupp2  30917  zarclsint  31225  zartopn  31228  zarmxt1  31233  zarcmplem  31234  dmsigagen  31513  measbase  31566  sseqf  31760  ballotlem7  31903  nosupno  33316  nosupdm  33317  nosupbday  33318  nosupres  33320  nosupbnd1lem1  33321  bj-inftyexpitaudisj  34620  bj-inftyexpidisj  34625  bj-elccinfty  34629  bj-minftyccb  34640  fin2so  35044  poimirlem30  35087  poimir  35090  dvtan  35107  itg2addnclem2  35109  ftc1anclem6  35135  totbndbnd  35227  comptiunov2i  40407  lhe4.4ex1a  41033  dvsinax  42555  fourierdlem62  42810  fourierdlem70  42818  fourierdlem71  42819  fourierdlem80  42828  fouriersw  42873  smflimsuplem1  43451  smflimsuplem4  43454  mndpsuppss  44773  scmsuppss  44774  lincext2  44864  aacllem  45329