Theorem dmmpti 6634

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  Vcvv 3438   ↦ cmpt 5177  dom cdm 5622

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-fun 6492  df-fn 6493

This theorem is referenced by:  fvmptex  6953  resfunexg  7159  brtpos2  8172  pwfilem  9216  inlresf  9824  inrresf  9826  vdwlem8  16914  oppccatf  17649  lubdm  18270  glbdm  18283  mndpsuppss  18688  dprd2dlem2  19969  dprd2dlem1  19970  dprd2da  19971  ablfac1c  20000  ablfac1eu  20002  ablfaclem2  20015  ablfaclem3  20016  elocv  21621  dmtopon  22865  dfac14  23560  kqtop  23687  symgtgp  24048  eltsms  24075  ressprdsds  24313  minveclem1  25378  isi1f  25629  itg1val  25638  cmvth  25949  cmvthOLD  25950  mvth  25951  lhop2  25974  dvfsumabs  25983  dvfsumrlim2  25993  taylthlem1  26335  taylthlem2  26336  taylthlem2OLD  26337  ulmdvlem1  26363  pige3ALT  26483  relogcn  26601  atandm  26840  atanf  26844  atancn  26900  dmarea  26921  dfarea  26924  efrlim  26933  efrlimOLD  26934  lgamgulmlem2  26994  dchrptlem2  27230  dchrptlem3  27231  dchrisum0  27485  nosupno  27669  nosupdm  27670  nosupbday  27671  nosupres  27673  nosupbnd1lem1  27674  noinfno  27684  noinfdm  27685  incistruhgr  29101  vsfval  30657  ipasslem8  30861  minvecolem1  30898  xppreima2  32678  ofpreima  32692  rmfsupp2  33269  zarclsint  33978  zartopn  33981  zarmxt1  33986  zarcmplem  33987  dmsigagen  34250  measbase  34303  sseqf  34498  ballotlem7  34642  bj-inftyexpitaudisj  37349  bj-inftyexpidisj  37354  bj-elccinfty  37358  bj-minftyccb  37369  fin2so  37747  poimirlem30  37790  poimir  37793  dvtan  37810  itg2addnclem2  37812  ftc1anclem6  37838  totbndbnd  37929  tfsconcatrev  43532  comptiunov2i  43889  lhe4.4ex1a  44512  dvsinax  46099  fourierdlem62  46354  fourierdlem70  46362  fourierdlem71  46363  fourierdlem80  46372  fouriersw  46417  smflimsuplem1  47006  smflimsuplem4  47009  scmsuppss  48559  lincext2  48643  idfurcl  49285  reldmprcof1  49568  reldmlmd2  49840  reldmcmd2  49841  aacllem  49988