Theorem dmmpti 6662

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3447   ↦ cmpt 5188  dom cdm 5638

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 5251  ax-nul 5261  ax-pr 5387

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-fun 6513  df-fn 6514

This theorem is referenced by:  fvmptex  6982  resfunexg  7189  brtpos2  8211  pwfilem  9267  inlresf  9867  inrresf  9869  vdwlem8  16959  oppccatf  17689  lubdm  18310  glbdm  18323  mndpsuppss  18692  dprd2dlem2  19972  dprd2dlem1  19973  dprd2da  19974  ablfac1c  20003  ablfac1eu  20005  ablfaclem2  20018  ablfaclem3  20019  elocv  21577  dmtopon  22810  dfac14  23505  kqtop  23632  symgtgp  23993  eltsms  24020  ressprdsds  24259  minveclem1  25324  isi1f  25575  itg1val  25584  cmvth  25895  cmvthOLD  25896  mvth  25897  lhop2  25920  dvfsumabs  25929  dvfsumrlim2  25939  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  ulmdvlem1  26309  pige3ALT  26429  relogcn  26547  atandm  26786  atanf  26790  atancn  26846  dmarea  26867  dfarea  26870  efrlim  26879  efrlimOLD  26880  lgamgulmlem2  26940  dchrptlem2  27176  dchrptlem3  27177  dchrisum0  27431  nosupno  27615  nosupdm  27616  nosupbday  27617  nosupres  27619  nosupbnd1lem1  27620  noinfno  27630  noinfdm  27631  incistruhgr  29006  vsfval  30562  ipasslem8  30766  minvecolem1  30803  xppreima2  32575  ofpreima  32589  rmfsupp2  33189  zarclsint  33862  zartopn  33865  zarmxt1  33870  zarcmplem  33871  dmsigagen  34134  measbase  34187  sseqf  34383  ballotlem7  34527  bj-inftyexpitaudisj  37193  bj-inftyexpidisj  37198  bj-elccinfty  37202  bj-minftyccb  37213  fin2so  37601  poimirlem30  37644  poimir  37647  dvtan  37664  itg2addnclem2  37666  ftc1anclem6  37692  totbndbnd  37783  tfsconcatrev  43337  comptiunov2i  43695  lhe4.4ex1a  44318  dvsinax  45911  fourierdlem62  46166  fourierdlem70  46174  fourierdlem71  46175  fourierdlem80  46184  fouriersw  46229  smflimsuplem1  46818  smflimsuplem4  46821  scmsuppss  48359  lincext2  48444  idfurcl  49087  reldmprcof1  49370  reldmlmd2  49642  reldmcmd2  49643  aacllem  49790