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

Theorem dmmpti 6485
Description: Domain of the mapping operation. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypotheses
Ref Expression
fnmpti.1 𝐵 ∈ V
fnmpti.2 𝐹 = (𝑥𝐴𝐵)
Assertion
Ref Expression
dmmpti dom 𝐹 = 𝐴
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem dmmpti
StepHypRef Expression
1 fnmpti.1 . . 3 𝐵 ∈ V
2 fnmpti.2 . . 3 𝐹 = (𝑥𝐴𝐵)
31, 2fnmpti 6484 . 2 𝐹 Fn 𝐴
4 fndm 6448 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
53, 4ax-mp 5 1 dom 𝐹 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  wcel 2107  Vcvv 3493  cmpt 5137  dom cdm 5548   Fn wfn 6343
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-fun 6350  df-fn 6351
This theorem is referenced by:  fvmptex  6775  resfunexg  6970  brtpos2  7890  inlresf  9335  inrresf  9337  vdwlem8  16316  lubdm  17581  glbdm  17594  dprd2dlem2  19154  dprd2dlem1  19155  dprd2da  19156  ablfac1c  19185  ablfac1eu  19187  ablfaclem2  19200  ablfaclem3  19201  elocv  20804  dmtopon  21523  dfac14  22218  kqtop  22345  symgtgp  22706  eltsms  22733  ressprdsds  22973  minveclem1  24019  isi1f  24267  itg1val  24276  cmvth  24580  mvth  24581  lhop2  24604  dvfsumabs  24612  dvfsumrlim2  24621  taylthlem1  24953  taylthlem2  24954  ulmdvlem1  24980  pige3ALT  25097  relogcn  25213  atandm  25446  atanf  25450  atancn  25506  dmarea  25527  dfarea  25530  efrlim  25539  lgamgulmlem2  25599  dchrptlem2  25833  dchrptlem3  25834  dchrisum0  26088  incistruhgr  26856  vsfval  28402  ipasslem8  28606  minvecolem1  28643  xppreima2  30387  ofpreima  30402  rmfsupp2  30859  dmsigagen  31391  measbase  31444  sseqf  31638  ballotlem7  31781  nosupno  33191  nosupdm  33192  nosupbday  33193  nosupres  33195  nosupbnd1lem1  33196  bj-inftyexpitaudisj  34474  bj-inftyexpidisj  34479  bj-elccinfty  34483  bj-minftyccb  34494  fin2so  34866  poimirlem30  34909  poimir  34912  dvtan  34929  itg2addnclem2  34931  ftc1anclem6  34959  totbndbnd  35054  comptiunov2i  40036  lhe4.4ex1a  40646  dvsinax  42181  fourierdlem62  42438  fourierdlem70  42446  fourierdlem71  42447  fourierdlem80  42456  fouriersw  42501  smflimsuplem1  43079  smflimsuplem4  43082  mndpsuppss  44404  scmsuppss  44405  lincext2  44495  aacllem  44887
  Copyright terms: Public domain W3C validator