Theorem dmmpti 6677

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  Vcvv 3450   ↦ cmpt 5186  dom cdm 5655

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-pr 5398

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-fun 6535  df-fn 6536

This theorem is used by:  fvmptex  7002  resfunexg  7215  brtpos2  8231  pwfilem  9288  inlresf  9920  inrresf  9922  sgndm  15170  vdwlem8  17081  oppccatf  17817  lubdm  18438  glbdm  18451  mndpsuppss  18873  dprd2dlem2  20170  dprd2dlem1  20171  dprd2da  20172  ablfac1c  20201  ablfac1eu  20203  ablfaclem2  20216  ablfaclem3  20217  elocv  21882  dmtopon  23149  dfac14  23845  kqtop  23972  symgtgp  24333  eltsms  24360  ressprdsds  24598  minveclem1  25653  isi1f  25903  itg1val  25912  cmvth  26219  mvth  26220  lhop2  26243  dvfsumabs  26251  dvfsumrlim2  26260  taylthlem1  26610  taylthlem2  26611  ulmdvlem1  26637  pige3ALT  26758  relogcn  26876  atandm  27114  atanf  27118  atancn  27174  dmarea  27195  dfarea  27198  efrlim  27207  lgamgulmlem2  27267  dchrptlem2  27502  dchrptlem3  27503  dchrisum0  27757  nosupno  27940  nosupdm  27941  nosupbday  27942  nosupres  27944  nosupbnd1lem1  27945  noinfno  27955  noinfdm  27956  incistruhgr  29537  vsfval  31115  ipasslem8  31319  minvecolem1  31356  xppreima2  33125  ofpreima  33139  rmfsupp2  33678  zarclsint  34383  zartopn  34386  zarmxt1  34391  zarcmplem  34392  dmsigagen  34656  measbase  34709  sseqf  34904  ballotlem7  35048  bj-inftyexpitaudisj  37958  bj-inftyexpidisj  37963  bj-elccinfty  37967  bj-minftyccb  37978  fin2so  38362  poimirlem30  38400  poimir  38403  dvtan  38420  itg2addnclem2  38422  ftc1anclem6  38448  totbndbnd  38540  tfsconcatrev  44190  comptiunov2i  44547  lhe4.4ex1a  45154  dvsinax  46742  fourierdlem62  46997  fourierdlem70  47005  fourierdlem71  47006  fourierdlem80  47015  fouriersw  47060  smflimsuplem1  47649  smflimsuplem4  47652  scmsuppss  49302  lincext2  49386  idfurcl  50025  reldmprcof1  50308  reldmlmd2  50580  reldmcmd2  50581  aacllem  50773