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

Theorem dmmpti 5725
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 5724 . 2  |-  F  Fn  A
4 fndm 5693 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
53, 4ax-mp 5 1  |-  dom  F  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    e. wcel 1870   _Vcvv 3087    |-> cmpt 4484   dom cdm 4854    Fn wfn 5596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pr 4661
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-fun 5603  df-fn 5604
This theorem is referenced by:  fvmptex  5976  resfunexg  6145  brtpos2  6987  vdwlem8  14901  lubdm  16176  glbdm  16189  dprd2dlem2  17608  dprd2dlem1  17609  dprd2da  17610  ablfac1c  17639  ablfac1eu  17641  ablfaclem2  17654  ablfaclem3  17655  elocv  19162  dfac14  20564  kqtop  20691  symgtgp  21047  eltsms  21078  ressprdsds  21317  minveclem1  22259  isi1f  22509  itg1val  22518  cmvth  22820  mvth  22821  lhop2  22844  dvfsumabs  22852  dvfsumrlim2  22861  taylthlem1  23193  taylthlem2  23194  ulmdvlem1  23220  pige3  23337  relogcn  23448  atandm  23667  atanf  23671  atancn  23727  dmarea  23748  dfarea  23751  efrlim  23760  lgamgulmlem2  23820  dchrptlem2  24056  dchrptlem3  24057  dchrisum0  24221  eleenn  24772  vsfval  26099  ipasslem8  26323  minvecolem1  26361  xppreima2  28089  ofpreima  28108  dmsigagen  28805  measbase  28858  sseqf  29051  ballotlem7  29194  bj-inftyexpidisj  31397  bj-elccinfty  31401  bj-minftyccb  31412  fin2so  31635  poimirlem30  31673  poimir  31676  dvtan  31695  itg2addnclem2  31697  ftc1anclem6  31725  totbndbnd  31824  comptiunov2i  35936  lhe4.4ex1a  36314  dvsinax  37354  fourierdlem62  37599  fourierdlem70  37607  fourierdlem71  37608  fourierdlem80  37617  fouriersw  37662  mndpsuppss  38915  scmsuppss  38916  lincext2  39007  aacllem  39300
  Copyright terms: Public domain W3C validator