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

Theorem dmmpti 5455
Description: Domain of an ordered-pair class abstraction that specifies a function. (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 5454 . 2  |-  F  Fn  A
4 fndm 5425 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
53, 4ax-mp 8 1  |-  dom  F  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1642    e. wcel 1710   _Vcvv 2864    e. cmpt 4158   dom cdm 4771    Fn wfn 5332
This theorem is referenced by:  fvmptex  5693  resfunexg  5823  brtpos2  6327  vdwlem8  13132  dprd2dlem2  15374  dprd2dlem1  15375  dprd2da  15376  ablfac1c  15405  ablfac1eu  15407  ablfaclem2  15420  ablfaclem3  15421  elocv  16674  dfac14  17418  kqtop  17542  symgtgp  17886  eltsms  17917  ressprdsds  18037  minveclem1  18892  isi1f  19133  itg1val  19142  cmvth  19442  mvth  19443  lhop2  19466  dvfsumabs  19474  dvfsumrlim2  19483  taylthlem1  19856  taylthlem2  19857  ulmdvlem1  19883  pige3  19992  relogcn  20096  atandm  20283  atanf  20287  atancn  20343  dmarea  20363  dfarea  20366  efrlim  20375  dchrptlem2  20616  dchrptlem3  20617  dchrisum0  20781  vsfval  21305  ipasslem8  21529  minvecolem1  21567  dmsigagen  23793  ballotlem7  24042  lgamgulmlem2  24063  eleenn  25083  itg2addnclem2  25493  areacirclem3  25518  totbndbnd  25836  lhe4.4ex1a  26869
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pr 4295
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-br 4105  df-opab 4159  df-mpt 4160  df-id 4391  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-fun 5339  df-fn 5340
  Copyright terms: Public domain W3C validator