Theorem dmmpti 6637

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  Vcvv 3430   ↦ cmpt 5167  dom cdm 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-fun 6495  df-fn 6496

This theorem is referenced by:  fvmptex  6957  resfunexg  7164  brtpos2  8176  pwfilem  9222  inlresf  9832  inrresf  9834  vdwlem8  16953  oppccatf  17688  lubdm  18309  glbdm  18322  mndpsuppss  18727  dprd2dlem2  20011  dprd2dlem1  20012  dprd2da  20013  ablfac1c  20042  ablfac1eu  20044  ablfaclem2  20057  ablfaclem3  20058  elocv  21661  dmtopon  22901  dfac14  23596  kqtop  23723  symgtgp  24084  eltsms  24111  ressprdsds  24349  minveclem1  25404  isi1f  25654  itg1val  25663  cmvth  25971  mvth  25972  lhop2  25995  dvfsumabs  26003  dvfsumrlim2  26012  taylthlem1  26353  taylthlem2  26354  taylthlem2OLD  26355  ulmdvlem1  26381  pige3ALT  26500  relogcn  26618  atandm  26856  atanf  26860  atancn  26916  dmarea  26937  dfarea  26940  efrlim  26949  efrlimOLD  26950  lgamgulmlem2  27010  dchrptlem2  27245  dchrptlem3  27246  dchrisum0  27500  nosupno  27684  nosupdm  27685  nosupbday  27686  nosupres  27688  nosupbnd1lem1  27689  noinfno  27699  noinfdm  27700  incistruhgr  29165  vsfval  30722  ipasslem8  30926  minvecolem1  30963  xppreima2  32742  ofpreima  32756  rmfsupp2  33317  zarclsint  34035  zartopn  34038  zarmxt1  34043  zarcmplem  34044  dmsigagen  34307  measbase  34360  sseqf  34555  ballotlem7  34699  bj-inftyexpitaudisj  37538  bj-inftyexpidisj  37543  bj-elccinfty  37547  bj-minftyccb  37558  fin2so  37945  poimirlem30  37988  poimir  37991  dvtan  38008  itg2addnclem2  38010  ftc1anclem6  38036  totbndbnd  38127  tfsconcatrev  43797  comptiunov2i  44154  lhe4.4ex1a  44777  dvsinax  46362  fourierdlem62  46617  fourierdlem70  46625  fourierdlem71  46626  fourierdlem80  46635  fouriersw  46680  smflimsuplem1  47269  smflimsuplem4  47272  scmsuppss  48862  lincext2  48946  idfurcl  49588  reldmprcof1  49871  reldmlmd2  50143  reldmcmd2  50144  aacllem  50291