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 2145  Vcvv 3451   ↦ cmpt 5186  dom cdm 5651

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 2733  ax-sep 5249  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-fun 6540  df-fn 6541

This theorem is used by:  fvmptex  7008  resfunexg  7221  brtpos2  8249  pwfilem  9309  inlresf  9995  inrresf  9997  sgndm  15249  vdwlem8  17166  oppccatf  17902  lubdm  18523  glbdm  18536  mndpsuppss  18959  dprd2dlem2  20256  dprd2dlem1  20257  dprd2da  20258  ablfac1c  20287  ablfac1eu  20289  ablfaclem2  20302  ablfaclem3  20303  elocv  21974  dmtopon  23241  dfac14  23937  kqtop  24064  symgtgp  24425  eltsms  24452  ressprdsds  24690  minveclem1  25745  isi1f  25995  itg1val  26004  cmvth  26311  mvth  26312  lhop2  26335  dvfsumabs  26343  dvfsumrlim2  26352  taylthlem1  26700  taylthlem2  26701  ulmdvlem1  26727  pige3ALT  26848  relogcn  26966  atandm  27204  atanf  27208  atancn  27264  dmarea  27285  dfarea  27288  efrlim  27297  lgamgulmlem2  27357  dchrptlem2  27592  dchrptlem3  27593  dchrisum0  27847  nosupno  28060  nosupdm  28061  nosupbday  28062  nosupres  28064  nosupbnd1lem1  28065  noinfno  28075  noinfdm  28076  incistruhgr  29657  vsfval  31235  ipasslem8  31439  minvecolem1  31476  xppreima2  33245  ofpreima  33259  rmfsupp2  33798  zarclsint  34504  zartopn  34507  zarmxt1  34512  zarcmplem  34513  dmsigagen  34777  measbase  34830  sseqf  35024  ballotlem7  35168  bj-inftyexpitaudisj  38126  bj-inftyexpidisj  38131  bj-elccinfty  38135  bj-minftyccb  38146  fin2so  38530  poimirlem30  38568  poimir  38571  dvtan  38588  itg2addnclem2  38590  ftc1anclem6  38616  totbndbnd  38723  tfsconcatrev  44349  comptiunov2i  44705  lhe4.4ex1a  45312  dvsinax  46922  fourierdlem62  47177  fourierdlem70  47185  fourierdlem71  47186  fourierdlem80  47195  fouriersw  47240  smflimsuplem1  47829  smflimsuplem4  47832  scmsuppss  49482  lincext2  49566  idfurcl  50205  reldmprcof1  50488  reldmlmd2  50760  reldmcmd2  50761  aacllem  50938