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

Theorem dmmpti 5692
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 5691 . 2  |-  F  Fn  A
4 fndm 5662 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
53, 4ax-mp 5 1  |-  dom  F  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398    e. wcel 1823   _Vcvv 3106    |-> cmpt 4497   dom cdm 4988    Fn wfn 5565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-fun 5572  df-fn 5573
This theorem is referenced by:  fvmptex  5942  resfunexg  6112  brtpos2  6953  vdwlem8  14593  lubdm  15811  glbdm  15824  dprd2dlem2  17287  dprd2dlem1  17288  dprd2da  17289  ablfac1c  17320  ablfac1eu  17322  ablfaclem2  17335  ablfaclem3  17336  elocv  18875  dfac14  20288  kqtop  20415  symgtgp  20769  eltsms  20800  ressprdsds  21043  minveclem1  22008  isi1f  22250  itg1val  22259  cmvth  22561  mvth  22562  lhop2  22585  dvfsumabs  22593  dvfsumrlim2  22602  taylthlem1  22937  taylthlem2  22938  ulmdvlem1  22964  pige3  23079  relogcn  23190  atandm  23407  atanf  23411  atancn  23467  dmarea  23488  dfarea  23491  efrlim  23500  dchrptlem2  23741  dchrptlem3  23742  dchrisum0  23906  eleenn  24404  vsfval  25729  ipasslem8  25953  minvecolem1  25991  xppreima2  27712  ofpreima  27737  dmsigagen  28377  measbase  28408  sseqf  28598  ballotlem7  28741  lgamgulmlem2  28839  fin2so  30283  dvtan  30308  itg2addnclem2  30310  ftc1anclem6  30338  totbndbnd  30528  lhe4.4ex1a  31478  dvsinax  31950  fourierdlem62  32193  fourierdlem70  32201  fourierdlem71  32202  fourierdlem80  32211  fouriersw  32256  mndpsuppss  33237  scmsuppss  33238  lincext2  33329  aacllem  33623  bj-inftyexpidisj  35032  bj-elccinfty  35036  bj-minftyccb  35047  comptiunov2i  38237
  Copyright terms: Public domain W3C validator