MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmmpti Structured version   Unicode version

Theorem dmmpti 5700
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
StepHypRef Expression
1 fnmpti.1 . . 3  |-  B  e. 
_V
2 fnmpti.2 . . 3  |-  F  =  ( x  e.  A  |->  B )
31, 2fnmpti 5699 . 2  |-  F  Fn  A
4 fndm 5670 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
53, 4ax-mp 5 1  |-  dom  F  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383    e. wcel 1804   _Vcvv 3095    |-> cmpt 4495   dom cdm 4989    Fn wfn 5573
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-fun 5580  df-fn 5581
This theorem is referenced by:  fvmptex  5951  resfunexg  6122  brtpos2  6963  vdwlem8  14488  lubdm  15588  glbdm  15601  dprd2dlem2  17068  dprd2dlem1  17069  dprd2da  17070  ablfac1c  17101  ablfac1eu  17103  ablfaclem2  17116  ablfaclem3  17117  elocv  18677  dfac14  20097  kqtop  20224  symgtgp  20578  eltsms  20609  ressprdsds  20852  minveclem1  21817  isi1f  22059  itg1val  22068  cmvth  22370  mvth  22371  lhop2  22394  dvfsumabs  22402  dvfsumrlim2  22411  taylthlem1  22746  taylthlem2  22747  ulmdvlem1  22773  pige3  22888  relogcn  22997  atandm  23185  atanf  23189  atancn  23245  dmarea  23265  dfarea  23268  efrlim  23277  dchrptlem2  23518  dchrptlem3  23519  dchrisum0  23683  eleenn  24177  vsfval  25506  ipasslem8  25730  minvecolem1  25768  xppreima2  27466  ofpreima  27485  dmsigagen  28122  measbase  28146  sseqf  28309  ballotlem7  28452  lgamgulmlem2  28550  fin2so  30016  dvtan  30041  itg2addnclem2  30043  ftc1anclem6  30071  totbndbnd  30261  lhe4.4ex1a  31210  dvsinax  31662  fourierdlem62  31905  fourierdlem70  31913  fourierdlem71  31914  fourierdlem80  31923  fouriersw  31968  mndpsuppss  32834  scmsuppss  32835  lincext2  32926  bj-inftyexpidisj  34488  bj-elccinfty  34492  bj-minftyccb  34503
  Copyright terms: Public domain W3C validator