Theorem dmmpti 6494

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

Syntax hints:   = wceq 1537   ∈ wcel 2114  Vcvv 3496   ↦ cmpt 5148  dom cdm 5557   Fn wfn 6352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-fun 6359  df-fn 6360

This theorem is referenced by:  fvmptex  6784  resfunexg  6980  brtpos2  7900  inlresf  9345  inrresf  9347  vdwlem8  16326  lubdm  17591  glbdm  17604  dprd2dlem2  19164  dprd2dlem1  19165  dprd2da  19166  ablfac1c  19195  ablfac1eu  19197  ablfaclem2  19210  ablfaclem3  19211  elocv  20814  dmtopon  21533  dfac14  22228  kqtop  22355  symgtgp  22716  eltsms  22743  ressprdsds  22983  minveclem1  24029  isi1f  24277  itg1val  24286  cmvth  24590  mvth  24591  lhop2  24614  dvfsumabs  24622  dvfsumrlim2  24631  taylthlem1  24963  taylthlem2  24964  ulmdvlem1  24990  pige3ALT  25107  relogcn  25223  atandm  25456  atanf  25460  atancn  25516  dmarea  25537  dfarea  25540  efrlim  25549  lgamgulmlem2  25609  dchrptlem2  25843  dchrptlem3  25844  dchrisum0  26098  incistruhgr  26866  vsfval  28412  ipasslem8  28616  minvecolem1  28653  xppreima2  30397  ofpreima  30412  rmfsupp2  30868  dmsigagen  31405  measbase  31458  sseqf  31652  ballotlem7  31795  nosupno  33205  nosupdm  33206  nosupbday  33207  nosupres  33209  nosupbnd1lem1  33210  bj-inftyexpitaudisj  34489  bj-inftyexpidisj  34494  bj-elccinfty  34498  bj-minftyccb  34509  fin2so  34881  poimirlem30  34924  poimir  34927  dvtan  34944  itg2addnclem2  34946  ftc1anclem6  34974  totbndbnd  35069  comptiunov2i  40058  lhe4.4ex1a  40668  dvsinax  42204  fourierdlem62  42460  fourierdlem70  42468  fourierdlem71  42469  fourierdlem80  42478  fouriersw  42523  smflimsuplem1  43101  smflimsuplem4  43104  mndpsuppss  44426  scmsuppss  44427  lincext2  44517  aacllem  44909