Theorem dmmpti 6682

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

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

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 5407

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 5559  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-fun 6541  df-fn 6542

This theorem is referenced by:  fvmptex  7007  resfunexg  7216  brtpos2  8230  pwfilem  9279  inlresf  9902  inrresf  9904  sgndm  15135  vdwlem8  17050  oppccatf  17786  lubdm  18407  glbdm  18420  mndpsuppss  18825  dprd2dlem2  20114  dprd2dlem1  20115  dprd2da  20116  ablfac1c  20145  ablfac1eu  20147  ablfaclem2  20160  ablfaclem3  20161  elocv  21789  dmtopon  23051  dfac14  23746  kqtop  23873  symgtgp  24234  eltsms  24261  ressprdsds  24499  minveclem1  25554  isi1f  25804  itg1val  25813  cmvth  26121  mvth  26122  lhop2  26145  dvfsumabs  26153  dvfsumrlim2  26162  taylthlem1  26504  taylthlem2  26505  ulmdvlem1  26531  pige3ALT  26653  relogcn  26771  atandm  27009  atanf  27013  atancn  27069  dmarea  27090  dfarea  27093  efrlim  27102  lgamgulmlem2  27162  dchrptlem2  27397  dchrptlem3  27398  dchrisum0  27652  nosupno  27835  nosupdm  27836  nosupbday  27837  nosupres  27839  nosupbnd1lem1  27840  noinfno  27850  noinfdm  27851  incistruhgr  29372  vsfval  30928  ipasslem8  31132  minvecolem1  31169  xppreima2  32939  ofpreima  32953  rmfsupp2  33500  zarclsint  34209  zartopn  34212  zarmxt1  34217  zarcmplem  34218  dmsigagen  34481  measbase  34534  sseqf  34729  ballotlem7  34873  bj-inftyexpitaudisj  37774  bj-inftyexpidisj  37779  bj-elccinfty  37783  bj-minftyccb  37794  fin2so  38183  poimirlem30  38226  poimir  38229  dvtan  38246  itg2addnclem2  38248  ftc1anclem6  38274  totbndbnd  38365  tfsconcatrev  44004  comptiunov2i  44361  lhe4.4ex1a  44968  dvsinax  46556  fourierdlem62  46811  fourierdlem70  46819  fourierdlem71  46820  fourierdlem80  46829  fouriersw  46874  smflimsuplem1  47463  smflimsuplem4  47466  scmsuppss  49073  lincext2  49157  idfurcl  49798  reldmprcof1  50081  reldmlmd2  50353  reldmcmd2  50354  aacllem  50512