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

Theorem dmmpti 5577
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 5576 . 2  |-  F  Fn  A
4 fndm 5547 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
53, 4ax-mp 5 1  |-  dom  F  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1653    e. wcel 1726   _Vcvv 2958    e. cmpt 4269   dom cdm 4881    Fn wfn 5452
This theorem is referenced by:  fvmptex  5818  resfunexg  5960  brtpos2  6488  vdwlem8  13361  dprd2dlem2  15603  dprd2dlem1  15604  dprd2da  15605  ablfac1c  15634  ablfac1eu  15636  ablfaclem2  15649  ablfaclem3  15650  elocv  16900  dfac14  17655  kqtop  17782  symgtgp  18136  eltsms  18167  ressprdsds  18406  minveclem1  19330  isi1f  19569  itg1val  19578  cmvth  19880  mvth  19881  lhop2  19904  dvfsumabs  19912  dvfsumrlim2  19921  taylthlem1  20294  taylthlem2  20295  ulmdvlem1  20321  pige3  20430  relogcn  20534  atandm  20721  atanf  20725  atancn  20781  dmarea  20801  dfarea  20804  efrlim  20813  dchrptlem2  21054  dchrptlem3  21055  dchrisum0  21219  vsfval  22119  ipasslem8  22343  minvecolem1  22381  xppreima2  24065  ofpreima  24086  dmsigagen  24532  measbase  24556  ballotlem7  24798  lgamgulmlem2  24819  eleenn  25840  dvtan  26269  itg2addnclem2  26271  ftc1anclem6  26299  totbndbnd  26512  lhe4.4ex1a  27537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pr 4406
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-fun 5459  df-fn 5460
  Copyright terms: Public domain W3C validator