Theorem dmmpti 6713

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  Vcvv 3454   ↦ cmpt 5192  dom cdm 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-fun 6568  df-fn 6569

This theorem is used by:  fvmptex  7039  resfunexg  7252  brtpos2  8287  pwfilem  9347  inlresf  10032  inrresf  10034  sgndm  15292  vdwlem8  17210  oppccatf  17952  lubdm  18573  glbdm  18586  mndpsuppss  19009  dprd2dlem2  20307  dprd2dlem1  20308  dprd2da  20309  ablfac1c  20338  ablfac1eu  20340  ablfaclem2  20353  ablfaclem3  20354  elocv  22029  dmtopon  23296  dfac14  23992  kqtop  24119  symgtgp  24480  eltsms  24507  ressprdsds  24745  minveclem1  25800  isi1f  26050  itg1val  26059  cmvth  26366  mvth  26367  lhop2  26390  dvfsumabs  26398  dvfsumrlim2  26407  taylthlem1  26757  taylthlem2  26758  ulmdvlem1  26784  pige3ALT  26905  relogcn  27023  atandm  27261  atanf  27265  atancn  27321  dmarea  27342  dfarea  27345  efrlim  27354  lgamgulmlem2  27414  dchrptlem2  27649  dchrptlem3  27650  dchrisum0  27904  nosupno  28117  nosupdm  28118  nosupbday  28119  nosupres  28121  nosupbnd1lem1  28122  noinfno  28132  noinfdm  28133  incistruhgr  29714  vsfval  31292  ipasslem8  31496  minvecolem1  31533  xppreima2  33343  ofpreima  33357  rmfsupp2  33897  zarclsint  34615  zartopn  34618  zarmxt1  34623  zarcmplem  34624  dmsigagen  34888  measbase  34941  sseqf  35135  ballotlem7  35279  bj-inftyexpitaudisj  38394  bj-inftyexpidisj  38399  bj-elccinfty  38403  bj-minftyccb  38414  fin2so  38798  poimirlem30  38836  poimir  38839  dvtan  38856  itg2addnclem2  38858  ftc1anclem6  38884  totbndbnd  38989  tfsconcatrev  44611  comptiunov2i  44967  lhe4.4ex1a  45574  dvsinax  47196  fourierdlem62  47451  fourierdlem70  47459  fourierdlem71  47460  fourierdlem80  47469  fouriersw  47514  smflimsuplem1  48103  smflimsuplem4  48106  scmsuppss  49814  lincext2  49898  idfurcl  50545  reldmprcof1  50847  reldmlmd2  51167  reldmcmd2  51168  aacllem  51367