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  17669  lubdm  18290  glbdm  18303  mndpsuppss  18674  dprd2dlem2  19956  dprd2dlem1  19957  dprd2da  19958  ablfac1c  19987  ablfac1eu  19989  ablfaclem2  20002  ablfaclem3  20003  elocv  21610  dmtopon  22843  dfac14  23538  kqtop  23665  symgtgp  24026  eltsms  24053  ressprdsds  24292  minveclem1  25357  isi1f  25608  itg1val  25617  cmvth  25928  cmvthOLD  25929  mvth  25930  lhop2  25953  dvfsumabs  25962  dvfsumrlim2  25972  taylthlem1  26314  taylthlem2  26315  taylthlem2OLD  26316  ulmdvlem1  26342  pige3ALT  26462  relogcn  26580  atandm  26819  atanf  26823  atancn  26879  dmarea  26900  dfarea  26903  efrlim  26912  efrlimOLD  26913  lgamgulmlem2  26973  dchrptlem2  27209  dchrptlem3  27210  dchrisum0  27464  nosupno  27648  nosupdm  27649  nosupbday  27650  nosupres  27652  nosupbnd1lem1  27653  noinfno  27663  noinfdm  27664  incistruhgr  29059  vsfval  30612  ipasslem8  30816  minvecolem1  30853  xppreima2  32625  ofpreima  32639  rmfsupp2  33205  zarclsint  33855  zartopn  33858  zarmxt1  33863  zarcmplem  33864  dmsigagen  34127  measbase  34180  sseqf  34376  ballotlem7  34520  bj-inftyexpitaudisj  37186  bj-inftyexpidisj  37191  bj-elccinfty  37195  bj-minftyccb  37206  fin2so  37594  poimirlem30  37637  poimir  37640  dvtan  37657  itg2addnclem2  37659  ftc1anclem6  37685  totbndbnd  37776  tfsconcatrev  43330  comptiunov2i  43688  lhe4.4ex1a  44311  dvsinax  45904  fourierdlem62  46159  fourierdlem70  46167  fourierdlem71  46168  fourierdlem80  46177  fouriersw  46222  smflimsuplem1  46811  smflimsuplem4  46814  scmsuppss  48352  lincext2  48437  idfurcl  49080  reldmprcof1  49363  reldmlmd2  49635  reldmcmd2  49636  aacllem  49783