Theorem dmmpti 6636

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  Vcvv 3440   ↦ cmpt 5179  dom cdm 5624

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 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-fun 6494  df-fn 6495

This theorem is referenced by:  fvmptex  6955  resfunexg  7161  brtpos2  8174  pwfilem  9218  inlresf  9826  inrresf  9828  vdwlem8  16916  oppccatf  17651  lubdm  18272  glbdm  18285  mndpsuppss  18690  dprd2dlem2  19971  dprd2dlem1  19972  dprd2da  19973  ablfac1c  20002  ablfac1eu  20004  ablfaclem2  20017  ablfaclem3  20018  elocv  21623  dmtopon  22867  dfac14  23562  kqtop  23689  symgtgp  24050  eltsms  24077  ressprdsds  24315  minveclem1  25380  isi1f  25631  itg1val  25640  cmvth  25951  cmvthOLD  25952  mvth  25953  lhop2  25976  dvfsumabs  25985  dvfsumrlim2  25995  taylthlem1  26337  taylthlem2  26338  taylthlem2OLD  26339  ulmdvlem1  26365  pige3ALT  26485  relogcn  26603  atandm  26842  atanf  26846  atancn  26902  dmarea  26923  dfarea  26926  efrlim  26935  efrlimOLD  26936  lgamgulmlem2  26996  dchrptlem2  27232  dchrptlem3  27233  dchrisum0  27487  nosupno  27671  nosupdm  27672  nosupbday  27673  nosupres  27675  nosupbnd1lem1  27676  noinfno  27686  noinfdm  27687  incistruhgr  29152  vsfval  30708  ipasslem8  30912  minvecolem1  30949  xppreima2  32729  ofpreima  32743  rmfsupp2  33320  zarclsint  34029  zartopn  34032  zarmxt1  34037  zarcmplem  34038  dmsigagen  34301  measbase  34354  sseqf  34549  ballotlem7  34693  bj-inftyexpitaudisj  37410  bj-inftyexpidisj  37415  bj-elccinfty  37419  bj-minftyccb  37430  fin2so  37808  poimirlem30  37851  poimir  37854  dvtan  37871  itg2addnclem2  37873  ftc1anclem6  37899  totbndbnd  37990  tfsconcatrev  43600  comptiunov2i  43957  lhe4.4ex1a  44580  dvsinax  46167  fourierdlem62  46422  fourierdlem70  46430  fourierdlem71  46431  fourierdlem80  46440  fouriersw  46485  smflimsuplem1  47074  smflimsuplem4  47077  scmsuppss  48627  lincext2  48711  idfurcl  49353  reldmprcof1  49636  reldmlmd2  49908  reldmcmd2  49909  aacllem  50056