Theorem dmmpti 6679

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

Syntax hints:   = wceq 1570   ∈ wcel 2143  Vcvv 3455   ↦ cmpt 5192  dom cdm 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-fun 6538  df-fn 6539

This theorem is referenced by:  fvmptex  7004  resfunexg  7213  brtpos2  8224  pwfilem  9273  inlresf  9896  inrresf  9898  sgndm  15129  vdwlem8  17043  oppccatf  17779  lubdm  18400  glbdm  18413  mndpsuppss  18818  dprd2dlem2  20107  dprd2dlem1  20108  dprd2da  20109  ablfac1c  20138  ablfac1eu  20140  ablfaclem2  20153  ablfaclem3  20154  elocv  21818  dmtopon  23080  dfac14  23775  kqtop  23902  symgtgp  24263  eltsms  24290  ressprdsds  24528  minveclem1  25583  isi1f  25833  itg1val  25842  cmvth  26150  mvth  26151  lhop2  26174  dvfsumabs  26182  dvfsumrlim2  26191  taylthlem1  26536  taylthlem2  26537  ulmdvlem1  26563  pige3ALT  26685  relogcn  26803  atandm  27041  atanf  27045  atancn  27101  dmarea  27122  dfarea  27125  efrlim  27134  lgamgulmlem2  27194  dchrptlem2  27429  dchrptlem3  27430  dchrisum0  27684  nosupno  27867  nosupdm  27868  nosupbday  27869  nosupres  27871  nosupbnd1lem1  27872  noinfno  27882  noinfdm  27883  incistruhgr  29429  vsfval  30985  ipasslem8  31189  minvecolem1  31226  xppreima2  32996  ofpreima  33010  rmfsupp2  33557  zarclsint  34262  zartopn  34265  zarmxt1  34270  zarcmplem  34271  dmsigagen  34534  measbase  34587  sseqf  34782  ballotlem7  34926  bj-inftyexpitaudisj  37849  bj-inftyexpidisj  37854  bj-elccinfty  37858  bj-minftyccb  37869  fin2so  38258  poimirlem30  38301  poimir  38304  dvtan  38321  itg2addnclem2  38323  ftc1anclem6  38349  totbndbnd  38440  tfsconcatrev  44075  comptiunov2i  44432  lhe4.4ex1a  45039  dvsinax  46627  fourierdlem62  46882  fourierdlem70  46890  fourierdlem71  46891  fourierdlem80  46900  fouriersw  46945  smflimsuplem1  47534  smflimsuplem4  47537  scmsuppss  49151  lincext2  49235  idfurcl  49876  reldmprcof1  50159  reldmlmd2  50431  reldmcmd2  50432  aacllem  50621