Theorem dmmpti 6665

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3450   ↦ cmpt 5191  dom cdm 5641

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-fun 6516  df-fn 6517

This theorem is referenced by:  fvmptex  6985  resfunexg  7192  brtpos2  8214  pwfilem  9274  inlresf  9874  inrresf  9876  vdwlem8  16966  oppccatf  17696  lubdm  18317  glbdm  18330  mndpsuppss  18699  dprd2dlem2  19979  dprd2dlem1  19980  dprd2da  19981  ablfac1c  20010  ablfac1eu  20012  ablfaclem2  20025  ablfaclem3  20026  elocv  21584  dmtopon  22817  dfac14  23512  kqtop  23639  symgtgp  24000  eltsms  24027  ressprdsds  24266  minveclem1  25331  isi1f  25582  itg1val  25591  cmvth  25902  cmvthOLD  25903  mvth  25904  lhop2  25927  dvfsumabs  25936  dvfsumrlim2  25946  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  ulmdvlem1  26316  pige3ALT  26436  relogcn  26554  atandm  26793  atanf  26797  atancn  26853  dmarea  26874  dfarea  26877  efrlim  26886  efrlimOLD  26887  lgamgulmlem2  26947  dchrptlem2  27183  dchrptlem3  27184  dchrisum0  27438  nosupno  27622  nosupdm  27623  nosupbday  27624  nosupres  27626  nosupbnd1lem1  27627  noinfno  27637  noinfdm  27638  incistruhgr  29013  vsfval  30569  ipasslem8  30773  minvecolem1  30810  xppreima2  32582  ofpreima  32596  rmfsupp2  33196  zarclsint  33869  zartopn  33872  zarmxt1  33877  zarcmplem  33878  dmsigagen  34141  measbase  34194  sseqf  34390  ballotlem7  34534  bj-inftyexpitaudisj  37200  bj-inftyexpidisj  37205  bj-elccinfty  37209  bj-minftyccb  37220  fin2so  37608  poimirlem30  37651  poimir  37654  dvtan  37671  itg2addnclem2  37673  ftc1anclem6  37699  totbndbnd  37790  tfsconcatrev  43344  comptiunov2i  43702  lhe4.4ex1a  44325  dvsinax  45918  fourierdlem62  46173  fourierdlem70  46181  fourierdlem71  46182  fourierdlem80  46191  fouriersw  46236  smflimsuplem1  46825  smflimsuplem4  46828  scmsuppss  48363  lincext2  48448  idfurcl  49091  reldmprcof1  49374  reldmlmd2  49646  reldmcmd2  49647  aacllem  49794