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

Theorem dmmpti 5540
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 5539 . 2  |-  F  Fn  A
4 fndm 5510 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
53, 4ax-mp 5 1  |-  dom  F  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369    e. wcel 1756   _Vcvv 2972    e. cmpt 4350   dom cdm 4840    Fn wfn 5413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pr 4531
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-fun 5420  df-fn 5421
This theorem is referenced by:  fvmptex  5784  resfunexg  5943  brtpos2  6751  vdwlem8  14049  lubdm  15149  glbdm  15162  dprd2dlem2  16539  dprd2dlem1  16540  dprd2da  16541  ablfac1c  16572  ablfac1eu  16574  ablfaclem2  16587  ablfaclem3  16588  elocv  18093  dfac14  19191  kqtop  19318  symgtgp  19672  eltsms  19703  ressprdsds  19946  minveclem1  20911  isi1f  21152  itg1val  21161  cmvth  21463  mvth  21464  lhop2  21487  dvfsumabs  21495  dvfsumrlim2  21504  taylthlem1  21838  taylthlem2  21839  ulmdvlem1  21865  pige3  21979  relogcn  22083  atandm  22271  atanf  22275  atancn  22331  dmarea  22351  dfarea  22354  efrlim  22363  dchrptlem2  22604  dchrptlem3  22605  dchrisum0  22769  eleenn  23142  vsfval  24013  ipasslem8  24237  minvecolem1  24275  xppreima2  25965  ofpreima  25984  dmsigagen  26587  measbase  26611  ballotlem7  26918  lgamgulmlem2  27016  fin2so  28416  dvtan  28442  itg2addnclem2  28444  ftc1anclem6  28472  totbndbnd  28688  lhe4.4ex1a  29603  mndpsuppss  30784  scmsuppss  30785  lincext2  30989  bj-inftyexpidisj  32533  bj-elccinfty  32537  bj-minftyccb  32548
  Copyright terms: Public domain W3C validator