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

Theorem dmmpti 5537
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 5536 . 2  |-  F  Fn  A
4 fndm 5507 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
53, 4ax-mp 5 1  |-  dom  F  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1364    e. wcel 1761   _Vcvv 2970    e. cmpt 4347   dom cdm 4836    Fn wfn 5410
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pr 4528
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-fun 5417  df-fn 5418
This theorem is referenced by:  fvmptex  5781  resfunexg  5940  brtpos2  6750  vdwlem8  14045  lubdm  15145  glbdm  15158  dprd2dlem2  16529  dprd2dlem1  16530  dprd2da  16531  ablfac1c  16562  ablfac1eu  16564  ablfaclem2  16577  ablfaclem3  16578  elocv  17993  dfac14  19091  kqtop  19218  symgtgp  19572  eltsms  19603  ressprdsds  19846  minveclem1  20811  isi1f  21052  itg1val  21061  cmvth  21363  mvth  21364  lhop2  21387  dvfsumabs  21395  dvfsumrlim2  21404  taylthlem1  21781  taylthlem2  21782  ulmdvlem1  21808  pige3  21922  relogcn  22026  atandm  22214  atanf  22218  atancn  22274  dmarea  22294  dfarea  22297  efrlim  22306  dchrptlem2  22547  dchrptlem3  22548  dchrisum0  22712  eleenn  23061  vsfval  23932  ipasslem8  24156  minvecolem1  24194  xppreima2  25884  ofpreima  25903  dmsigagen  26507  measbase  26531  ballotlem7  26832  lgamgulmlem2  26930  fin2so  28325  dvtan  28351  itg2addnclem2  28353  ftc1anclem6  28381  totbndbnd  28597  lhe4.4ex1a  29512  mndpsuppss  30684  scmsuppss  30685  lincext2  30813  bj-inftyexpidisj  32228  bj-elccinfty  32232  bj-minftyccb  32243
  Copyright terms: Public domain W3C validator