Theorem dmmpti 6260

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 6259	. 2 ⊢ 𝐹 Fn 𝐴
4		fndm 6227	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
5	3, 4	ax-mp 5	1 ⊢ dom 𝐹 = 𝐴

Syntax hints:   = wceq 1656   ∈ wcel 2164  Vcvv 3414   ↦ cmpt 4954  dom cdm 5346   Fn wfn 6122

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5007  ax-nul 5015  ax-pr 5129

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-sn 4400  df-pr 4402  df-op 4406  df-br 4876  df-opab 4938  df-mpt 4955  df-id 5252  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-fun 6129  df-fn 6130

This theorem is referenced by:  fvmptex  6546  resfunexg  6740  brtpos2  7628  inlresf  9060  inrresf  9062  vdwlem8  16070  lubdm  17339  glbdm  17352  dprd2dlem2  18800  dprd2dlem1  18801  dprd2da  18802  ablfac1c  18831  ablfac1eu  18833  ablfaclem2  18846  ablfaclem3  18847  elocv  20382  dmtopon  21105  dfac14  21799  kqtop  21926  symgtgp  22282  eltsms  22313  ressprdsds  22553  minveclem1  23599  isi1f  23847  itg1val  23856  cmvth  24160  mvth  24161  lhop2  24184  dvfsumabs  24192  dvfsumrlim2  24201  taylthlem1  24533  taylthlem2  24534  ulmdvlem1  24560  pige3  24676  relogcn  24790  atandm  25023  atanf  25027  atancn  25083  dmarea  25104  dfarea  25107  efrlim  25116  lgamgulmlem2  25176  dchrptlem2  25410  dchrptlem3  25411  dchrisum0  25629  eleenn  26202  incistruhgr  26384  vsfval  28039  ipasslem8  28243  minvecolem1  28281  xppreima2  29995  ofpreima  30010  dmsigagen  30748  measbase  30801  sseqf  30996  ballotlem7  31139  nosupno  32383  nosupdm  32384  nosupbday  32385  nosupres  32387  nosupbnd1lem1  32388  bj-inftyexpitaudisj  33627  bj-inftyexpidisj  33632  bj-elccinfty  33636  bj-minftyccb  33647  fin2so  33934  poimirlem30  33978  poimir  33981  dvtan  33998  itg2addnclem2  34000  ftc1anclem6  34028  totbndbnd  34125  comptiunov2i  38834  lhe4.4ex1a  39363  dvsinax  40916  fourierdlem62  41173  fourierdlem70  41181  fourierdlem71  41182  fourierdlem80  41191  fouriersw  41236  smflimsuplem1  41814  smflimsuplem4  41817  mndpsuppss  43013  scmsuppss  43014  lincext2  43105  aacllem  43453