Theorem dmmpti 6712

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  Vcvv 3480   ↦ cmpt 5225  dom cdm 5685

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-fun 6563  df-fn 6564

This theorem is referenced by:  fvmptex  7030  resfunexg  7235  brtpos2  8257  pwfilem  9356  inlresf  9954  inrresf  9956  vdwlem8  17026  oppccatf  17771  lubdm  18396  glbdm  18409  mndpsuppss  18778  dprd2dlem2  20060  dprd2dlem1  20061  dprd2da  20062  ablfac1c  20091  ablfac1eu  20093  ablfaclem2  20106  ablfaclem3  20107  elocv  21686  dmtopon  22929  dfac14  23626  kqtop  23753  symgtgp  24114  eltsms  24141  ressprdsds  24381  minveclem1  25458  isi1f  25709  itg1val  25718  cmvth  26029  cmvthOLD  26030  mvth  26031  lhop2  26054  dvfsumabs  26063  dvfsumrlim2  26073  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  ulmdvlem1  26443  pige3ALT  26562  relogcn  26680  atandm  26919  atanf  26923  atancn  26979  dmarea  27000  dfarea  27003  efrlim  27012  efrlimOLD  27013  lgamgulmlem2  27073  dchrptlem2  27309  dchrptlem3  27310  dchrisum0  27564  nosupno  27748  nosupdm  27749  nosupbday  27750  nosupres  27752  nosupbnd1lem1  27753  noinfno  27763  noinfdm  27764  incistruhgr  29096  vsfval  30652  ipasslem8  30856  minvecolem1  30893  xppreima2  32661  ofpreima  32675  rmfsupp2  33242  zarclsint  33871  zartopn  33874  zarmxt1  33879  zarcmplem  33880  dmsigagen  34145  measbase  34198  sseqf  34394  ballotlem7  34538  bj-inftyexpitaudisj  37206  bj-inftyexpidisj  37211  bj-elccinfty  37215  bj-minftyccb  37226  fin2so  37614  poimirlem30  37657  poimir  37660  dvtan  37677  itg2addnclem2  37679  ftc1anclem6  37705  totbndbnd  37796  tfsconcatrev  43361  comptiunov2i  43719  lhe4.4ex1a  44348  dvsinax  45928  fourierdlem62  46183  fourierdlem70  46191  fourierdlem71  46192  fourierdlem80  46201  fouriersw  46246  smflimsuplem1  46835  smflimsuplem4  46838  scmsuppss  48287  lincext2  48372  aacllem  49320