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

Theorem dmmpti 5919
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 5918 . 2 𝐹 Fn 𝐴
4 fndm 5887 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
53, 4ax-mp 5 1 dom 𝐹 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wcel 1976  Vcvv 3169  cmpt 4634  dom cdm 5025   Fn wfn 5782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pr 4825
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-br 4575  df-opab 4635  df-mpt 4636  df-id 4940  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-fun 5789  df-fn 5790
This theorem is referenced by:  fvmptex  6185  resfunexg  6359  brtpos2  7219  vdwlem8  15473  lubdm  16745  glbdm  16758  dprd2dlem2  18205  dprd2dlem1  18206  dprd2da  18207  ablfac1c  18236  ablfac1eu  18238  ablfaclem2  18251  ablfaclem3  18252  elocv  19770  dfac14  21170  kqtop  21297  symgtgp  21654  eltsms  21685  ressprdsds  21924  minveclem1  22917  isi1f  23161  itg1val  23170  cmvth  23472  mvth  23473  lhop2  23496  dvfsumabs  23504  dvfsumrlim2  23513  taylthlem1  23845  taylthlem2  23846  ulmdvlem1  23872  pige3  23987  relogcn  24098  atandm  24317  atanf  24321  atancn  24377  dmarea  24398  dfarea  24401  efrlim  24410  lgamgulmlem2  24470  dchrptlem2  24704  dchrptlem3  24705  dchrisum0  24923  eleenn  25491  vsfval  26655  ipasslem8  26879  minvecolem1  26917  xppreima2  28633  ofpreima  28651  dmsigagen  29337  measbase  29390  sseqf  29584  ballotlem7  29727  bj-dmtopon  32042  bj-inftyexpidisj  32074  bj-elccinfty  32078  bj-minftyccb  32089  fin2so  32366  poimirlem30  32409  poimir  32412  dvtan  32430  itg2addnclem2  32432  ftc1anclem6  32460  totbndbnd  32558  comptiunov2i  36817  lhe4.4ex1a  37350  dvsinax  38602  fourierdlem62  38862  fourierdlem70  38870  fourierdlem71  38871  fourierdlem80  38880  fouriersw  38925  incistruhgr  40304  mndpsuppss  41945  scmsuppss  41946  lincext2  42037  aacllem  42316
  Copyright terms: Public domain W3C validator