Theorem dmmpti 6023

Description: Domain of the mapping operation. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 31-Aug-2015.)

Hypotheses

Ref	Expression
fnmpti.1	|- B e. _V
fnmpti.2	|- F = ( x e. A |-> B )

Assertion

Ref	Expression
dmmpti	|- dom F = A

Distinct variable group:   x, A

Allowed substitution hints:   B( x)   F( x)

Proof of Theorem dmmpti

Step	Hyp	Ref	Expression
1		fnmpti.1	. . 3 |- B e. _V
2		fnmpti.2	. . 3 |- F = ( x e. A |-> B )
3	1, 2	fnmpti 6022	. 2 |- F Fn A
4		fndm 5990	. 2 |- ( F Fn A -> dom F = A )
5	3, 4	ax-mp 5	1 |- dom F = A

Syntax hints:   = wceq 1483   e. wcel 1990   _Vcvv 3200   |-> cmpt 4729   dom cdm 5114   Fn wfn 5883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-fun 5890  df-fn 5891

This theorem is referenced by:  fvmptex  6294  resfunexg  6479  brtpos2  7358  vdwlem8  15692  lubdm  16979  glbdm  16992  dprd2dlem2  18439  dprd2dlem1  18440  dprd2da  18441  ablfac1c  18470  ablfac1eu  18472  ablfaclem2  18485  ablfaclem3  18486  elocv  20012  dmtopon  20727  dfac14  21421  kqtop  21548  symgtgp  21905  eltsms  21936  ressprdsds  22176  minveclem1  23195  isi1f  23441  itg1val  23450  cmvth  23754  mvth  23755  lhop2  23778  dvfsumabs  23786  dvfsumrlim2  23795  taylthlem1  24127  taylthlem2  24128  ulmdvlem1  24154  pige3  24269  relogcn  24384  atandm  24603  atanf  24607  atancn  24663  dmarea  24684  dfarea  24687  efrlim  24696  lgamgulmlem2  24756  dchrptlem2  24990  dchrptlem3  24991  dchrisum0  25209  eleenn  25776  incistruhgr  25974  vsfval  27488  ipasslem8  27692  minvecolem1  27730  xppreima2  29450  ofpreima  29465  dmsigagen  30207  measbase  30260  sseqf  30454  ballotlem7  30597  nosupno  31849  nosupdm  31850  nosupbday  31851  nosupres  31853  nosupbnd1lem1  31854  bj-inftyexpidisj  33097  bj-elccinfty  33101  bj-minftyccb  33112  fin2so  33396  poimirlem30  33439  poimir  33442  dvtan  33460  itg2addnclem2  33462  ftc1anclem6  33490  totbndbnd  33588  comptiunov2i  37998  lhe4.4ex1a  38528  dvsinax  40127  fourierdlem62  40385  fourierdlem70  40393  fourierdlem71  40394  fourierdlem80  40403  fouriersw  40448  smflimsuplem1  41026  smflimsuplem4  41029  mndpsuppss  42152  scmsuppss  42153  lincext2  42244  aacllem  42547