Theorem dmmpti 6644

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3444   ↦ cmpt 5183  dom cdm 5631

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-fun 6501  df-fn 6502

This theorem is referenced by:  fvmptex  6964  resfunexg  7171  brtpos2  8188  pwfilem  9243  inlresf  9843  inrresf  9845  vdwlem8  16935  oppccatf  17665  lubdm  18286  glbdm  18299  mndpsuppss  18668  dprd2dlem2  19948  dprd2dlem1  19949  dprd2da  19950  ablfac1c  19979  ablfac1eu  19981  ablfaclem2  19994  ablfaclem3  19995  elocv  21553  dmtopon  22786  dfac14  23481  kqtop  23608  symgtgp  23969  eltsms  23996  ressprdsds  24235  minveclem1  25300  isi1f  25551  itg1val  25560  cmvth  25871  cmvthOLD  25872  mvth  25873  lhop2  25896  dvfsumabs  25905  dvfsumrlim2  25915  taylthlem1  26257  taylthlem2  26258  taylthlem2OLD  26259  ulmdvlem1  26285  pige3ALT  26405  relogcn  26523  atandm  26762  atanf  26766  atancn  26822  dmarea  26843  dfarea  26846  efrlim  26855  efrlimOLD  26856  lgamgulmlem2  26916  dchrptlem2  27152  dchrptlem3  27153  dchrisum0  27407  nosupno  27591  nosupdm  27592  nosupbday  27593  nosupres  27595  nosupbnd1lem1  27596  noinfno  27606  noinfdm  27607  incistruhgr  28982  vsfval  30535  ipasslem8  30739  minvecolem1  30776  xppreima2  32548  ofpreima  32562  rmfsupp2  33162  zarclsint  33835  zartopn  33838  zarmxt1  33843  zarcmplem  33844  dmsigagen  34107  measbase  34160  sseqf  34356  ballotlem7  34500  bj-inftyexpitaudisj  37166  bj-inftyexpidisj  37171  bj-elccinfty  37175  bj-minftyccb  37186  fin2so  37574  poimirlem30  37617  poimir  37620  dvtan  37637  itg2addnclem2  37639  ftc1anclem6  37665  totbndbnd  37756  tfsconcatrev  43310  comptiunov2i  43668  lhe4.4ex1a  44291  dvsinax  45884  fourierdlem62  46139  fourierdlem70  46147  fourierdlem71  46148  fourierdlem80  46157  fouriersw  46202  smflimsuplem1  46791  smflimsuplem4  46794  scmsuppss  48332  lincext2  48417  idfurcl  49060  reldmprcof1  49343  reldmlmd2  49615  reldmcmd2  49616  aacllem  49763