Theorem dmmpti 6629

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

Syntax hints:   = wceq 1547   ∈ wcel 2119  Vcvv 3431   ↦ cmpt 5153  dom cdm 5618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-fun 6487  df-fn 6488

This theorem is referenced by:  fvmptex  6950  resfunexg  7159  brtpos2  8172  pwfilem  9218  inlresf  9829  inrresf  9831  vdwlem8  16950  oppccatf  17685  lubdm  18306  glbdm  18319  mndpsuppss  18724  dprd2dlem2  20008  dprd2dlem1  20009  dprd2da  20010  ablfac1c  20039  ablfac1eu  20041  ablfaclem2  20054  ablfaclem3  20055  elocv  21643  dmtopon  22906  dfac14  23601  kqtop  23728  symgtgp  24089  eltsms  24116  ressprdsds  24354  minveclem1  25409  isi1f  25659  itg1val  25668  cmvth  25976  mvth  25977  lhop2  26000  dvfsumabs  26008  dvfsumrlim2  26017  taylthlem1  26356  taylthlem2  26357  ulmdvlem1  26383  pige3ALT  26502  relogcn  26620  atandm  26858  atanf  26862  atancn  26918  dmarea  26939  dfarea  26942  efrlim  26951  lgamgulmlem2  27011  dchrptlem2  27246  dchrptlem3  27247  dchrisum0  27501  nosupno  27685  nosupdm  27686  nosupbday  27687  nosupres  27689  nosupbnd1lem1  27690  noinfno  27700  noinfdm  27701  incistruhgr  29166  vsfval  30722  ipasslem8  30926  minvecolem1  30963  xppreima2  32743  ofpreima  32757  rmfsupp2  33319  zarclsint  34056  zartopn  34059  zarmxt1  34064  zarcmplem  34065  dmsigagen  34328  measbase  34381  sseqf  34576  ballotlem7  34720  bj-inftyexpitaudisj  37565  bj-inftyexpidisj  37570  bj-elccinfty  37574  bj-minftyccb  37585  fin2so  37974  poimirlem30  38017  poimir  38020  dvtan  38037  itg2addnclem2  38039  ftc1anclem6  38065  totbndbnd  38156  tfsconcatrev  43793  comptiunov2i  44150  lhe4.4ex1a  44773  dvsinax  46356  fourierdlem62  46611  fourierdlem70  46619  fourierdlem71  46620  fourierdlem80  46629  fouriersw  46674  smflimsuplem1  47263  smflimsuplem4  47266  scmsuppss  48862  lincext2  48946  idfurcl  49588  reldmprcof1  49871  reldmlmd2  50143  reldmcmd2  50144  aacllem  50291