Theorem dmmpti 6680

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

Syntax hints:   = wceq 1567   ∈ wcel 2149  Vcvv 3463   ↦ cmpt 5196  dom cdm 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-fun 6539  df-fn 6540

This theorem is referenced by:  fvmptex  7005  resfunexg  7214  brtpos2  8227  pwfilem  9276  inlresf  9899  inrresf  9901  sgndm  15132  vdwlem8  17047  oppccatf  17783  lubdm  18404  glbdm  18417  mndpsuppss  18822  dprd2dlem2  20111  dprd2dlem1  20112  dprd2da  20113  ablfac1c  20142  ablfac1eu  20144  ablfaclem2  20157  ablfaclem3  20158  elocv  21786  dmtopon  23048  dfac14  23743  kqtop  23870  symgtgp  24231  eltsms  24258  ressprdsds  24496  minveclem1  25551  isi1f  25801  itg1val  25810  cmvth  26118  mvth  26119  lhop2  26142  dvfsumabs  26150  dvfsumrlim2  26159  taylthlem1  26501  taylthlem2  26502  ulmdvlem1  26528  pige3ALT  26650  relogcn  26768  atandm  27006  atanf  27010  atancn  27066  dmarea  27087  dfarea  27090  efrlim  27099  lgamgulmlem2  27159  dchrptlem2  27394  dchrptlem3  27395  dchrisum0  27649  nosupno  27832  nosupdm  27833  nosupbday  27834  nosupres  27836  nosupbnd1lem1  27837  noinfno  27847  noinfdm  27848  incistruhgr  29369  vsfval  30925  ipasslem8  31129  minvecolem1  31166  xppreima2  32936  ofpreima  32950  rmfsupp2  33497  zarclsint  34206  zartopn  34209  zarmxt1  34214  zarcmplem  34215  dmsigagen  34478  measbase  34531  sseqf  34726  ballotlem7  34870  bj-inftyexpitaudisj  37736  bj-inftyexpidisj  37741  bj-elccinfty  37745  bj-minftyccb  37756  fin2so  38145  poimirlem30  38188  poimir  38191  dvtan  38208  itg2addnclem2  38210  ftc1anclem6  38236  totbndbnd  38327  tfsconcatrev  43966  comptiunov2i  44323  lhe4.4ex1a  44930  dvsinax  46518  fourierdlem62  46773  fourierdlem70  46781  fourierdlem71  46782  fourierdlem80  46791  fouriersw  46836  smflimsuplem1  47425  smflimsuplem4  47428  scmsuppss  49035  lincext2  49119  idfurcl  49760  reldmprcof1  50043  reldmlmd2  50315  reldmcmd2  50316  aacllem  50474