Theorem dmmpti 6683

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  Vcvv 3457   ↦ cmpt 5194  dom cdm 5663

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-fun 6542  df-fn 6543

This theorem is used by:  fvmptex  7008  resfunexg  7220  brtpos2  8234  pwfilem  9284  inlresf  9916  inrresf  9918  sgndm  15157  vdwlem8  17070  oppccatf  17806  lubdm  18427  glbdm  18440  mndpsuppss  18860  dprd2dlem2  20156  dprd2dlem1  20157  dprd2da  20158  ablfac1c  20187  ablfac1eu  20189  ablfaclem2  20202  ablfaclem3  20203  elocv  21868  dmtopon  23130  dfac14  23826  kqtop  23953  symgtgp  24314  eltsms  24341  ressprdsds  24579  minveclem1  25634  isi1f  25884  itg1val  25893  cmvth  26201  mvth  26202  lhop2  26225  dvfsumabs  26233  dvfsumrlim2  26242  taylthlem1  26587  taylthlem2  26588  ulmdvlem1  26614  pige3ALT  26736  relogcn  26854  atandm  27092  atanf  27096  atancn  27152  dmarea  27173  dfarea  27176  efrlim  27185  lgamgulmlem2  27245  dchrptlem2  27480  dchrptlem3  27481  dchrisum0  27735  nosupno  27918  nosupdm  27919  nosupbday  27920  nosupres  27922  nosupbnd1lem1  27923  noinfno  27933  noinfdm  27934  incistruhgr  29484  vsfval  31056  ipasslem8  31260  minvecolem1  31297  xppreima2  33067  ofpreima  33081  rmfsupp2  33621  zarclsint  34326  zartopn  34329  zarmxt1  34334  zarcmplem  34335  dmsigagen  34599  measbase  34652  sseqf  34847  ballotlem7  34991  bj-inftyexpitaudisj  37906  bj-inftyexpidisj  37911  bj-elccinfty  37915  bj-minftyccb  37926  fin2so  38315  poimirlem30  38358  poimir  38361  dvtan  38378  itg2addnclem2  38380  ftc1anclem6  38406  totbndbnd  38498  tfsconcatrev  44133  comptiunov2i  44490  lhe4.4ex1a  45097  dvsinax  46685  fourierdlem62  46940  fourierdlem70  46948  fourierdlem71  46949  fourierdlem80  46958  fouriersw  47003  smflimsuplem1  47592  smflimsuplem4  47595  scmsuppss  49208  lincext2  49292  idfurcl  49933  reldmprcof1  50216  reldmlmd2  50488  reldmcmd2  50489  aacllem  50678