Theorem dmmpti 6626

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3436   ↦ cmpt 5173  dom cdm 5619

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 5235  ax-nul 5245  ax-pr 5371

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-fun 6484  df-fn 6485

This theorem is referenced by:  fvmptex  6944  resfunexg  7151  brtpos2  8165  pwfilem  9207  inlresf  9810  inrresf  9812  vdwlem8  16900  oppccatf  17634  lubdm  18255  glbdm  18268  mndpsuppss  18639  dprd2dlem2  19921  dprd2dlem1  19922  dprd2da  19923  ablfac1c  19952  ablfac1eu  19954  ablfaclem2  19967  ablfaclem3  19968  elocv  21575  dmtopon  22808  dfac14  23503  kqtop  23630  symgtgp  23991  eltsms  24018  ressprdsds  24257  minveclem1  25322  isi1f  25573  itg1val  25582  cmvth  25893  cmvthOLD  25894  mvth  25895  lhop2  25918  dvfsumabs  25927  dvfsumrlim2  25937  taylthlem1  26279  taylthlem2  26280  taylthlem2OLD  26281  ulmdvlem1  26307  pige3ALT  26427  relogcn  26545  atandm  26784  atanf  26788  atancn  26844  dmarea  26865  dfarea  26868  efrlim  26877  efrlimOLD  26878  lgamgulmlem2  26938  dchrptlem2  27174  dchrptlem3  27175  dchrisum0  27429  nosupno  27613  nosupdm  27614  nosupbday  27615  nosupres  27617  nosupbnd1lem1  27618  noinfno  27628  noinfdm  27629  incistruhgr  29024  vsfval  30577  ipasslem8  30781  minvecolem1  30818  xppreima2  32594  ofpreima  32608  rmfsupp2  33178  zarclsint  33839  zartopn  33842  zarmxt1  33847  zarcmplem  33848  dmsigagen  34111  measbase  34164  sseqf  34360  ballotlem7  34504  bj-inftyexpitaudisj  37179  bj-inftyexpidisj  37184  bj-elccinfty  37188  bj-minftyccb  37199  fin2so  37587  poimirlem30  37630  poimir  37633  dvtan  37650  itg2addnclem2  37652  ftc1anclem6  37678  totbndbnd  37769  tfsconcatrev  43321  comptiunov2i  43679  lhe4.4ex1a  44302  dvsinax  45894  fourierdlem62  46149  fourierdlem70  46157  fourierdlem71  46158  fourierdlem80  46167  fouriersw  46212  smflimsuplem1  46801  smflimsuplem4  46804  scmsuppss  48355  lincext2  48440  idfurcl  49083  reldmprcof1  49366  reldmlmd2  49638  reldmcmd2  49639  aacllem  49786