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

Theorem dmmpti 6162
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 6161 . 2 𝐹 Fn 𝐴
4 fndm 6129 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
53, 4ax-mp 5 1 dom 𝐹 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1629  wcel 2143  Vcvv 3348  cmpt 4860  dom cdm 5248   Fn wfn 6025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1868  ax-4 1883  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2152  ax-10 2172  ax-11 2188  ax-12 2201  ax-13 2406  ax-ext 2749  ax-sep 4911  ax-nul 4919  ax-pr 5033
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1071  df-tru 1632  df-ex 1851  df-nf 1856  df-sb 2048  df-eu 2620  df-mo 2621  df-clab 2756  df-cleq 2762  df-clel 2765  df-nfc 2900  df-ral 3064  df-rab 3068  df-v 3350  df-dif 3723  df-un 3725  df-in 3727  df-ss 3734  df-nul 4061  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-br 4784  df-opab 4844  df-mpt 4861  df-id 5156  df-xp 5254  df-rel 5255  df-cnv 5256  df-co 5257  df-dm 5258  df-fun 6032  df-fn 6033
This theorem is referenced by:  fvmptex  6435  resfunexg  6621  brtpos2  7508  inlresf  8938  inrresf  8940  vdwlem8  15905  lubdm  17193  glbdm  17206  dprd2dlem2  18653  dprd2dlem1  18654  dprd2da  18655  ablfac1c  18684  ablfac1eu  18686  ablfaclem2  18699  ablfaclem3  18700  elocv  20235  dmtopon  20954  dfac14  21648  kqtop  21775  symgtgp  22131  eltsms  22162  ressprdsds  22402  minveclem1  23420  isi1f  23667  itg1val  23676  cmvth  23980  mvth  23981  lhop2  24004  dvfsumabs  24012  dvfsumrlim2  24021  taylthlem1  24353  taylthlem2  24354  ulmdvlem1  24380  pige3  24496  relogcn  24611  atandm  24830  atanf  24834  atancn  24890  dmarea  24911  dfarea  24914  efrlim  24923  lgamgulmlem2  24983  dchrptlem2  25217  dchrptlem3  25218  dchrisum0  25436  eleenn  26003  incistruhgr  26201  vsfval  27829  ipasslem8  28033  minvecolem1  28071  xppreima2  29791  ofpreima  29806  dmsigagen  30548  measbase  30601  sseqf  30795  ballotlem7  30938  nosupno  32187  nosupdm  32188  nosupbday  32189  nosupres  32191  nosupbnd1lem1  32192  bj-inftyexpidisj  33434  bj-elccinfty  33438  bj-minftyccb  33449  fin2so  33729  poimirlem30  33772  poimir  33775  dvtan  33792  itg2addnclem2  33794  ftc1anclem6  33822  totbndbnd  33920  comptiunov2i  38524  lhe4.4ex1a  39054  dvsinax  40646  fourierdlem62  40903  fourierdlem70  40911  fourierdlem71  40912  fourierdlem80  40921  fouriersw  40966  smflimsuplem1  41547  smflimsuplem4  41550  mndpsuppss  42677  scmsuppss  42678  lincext2  42769  aacllem  43075
  Copyright terms: Public domain W3C validator