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

Theorem fdmi 5394
Description: The domain of a mapping. (Contributed by NM, 28-Jul-2008.)
Hypothesis
Ref Expression
fdmi.1  |-  F : A
--> B
Assertion
Ref Expression
fdmi  |-  dom  F  =  A

Proof of Theorem fdmi
StepHypRef Expression
1 fdmi.1 . 2  |-  F : A
--> B
2 fdm 5393 . 2  |-  ( F : A --> B  ->  dom  F  =  A )
31, 2ax-mp 8 1  |-  dom  F  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1623   dom cdm 4689   -->wf 5251
This theorem is referenced by:  f0cli  5671  rankvaln  7471  isnum2  7578  r0weon  7640  cfub  7875  cardcf  7878  cflecard  7879  cfle  7880  cflim2  7889  cfidm  7901  cardf  8172  smobeth  8208  inar1  8397  addcompq  8574  addcomnq  8575  mulcompq  8576  mulcomnq  8577  adderpq  8580  mulerpq  8581  addassnq  8582  mulassnq  8583  distrnq  8585  recmulnq  8588  recclnq  8590  dmrecnq  8592  lterpq  8594  ltanq  8595  ltmnq  8596  ltexnq  8599  nsmallnq  8601  ltbtwnnq  8602  prlem934  8657  ltaddpr  8658  ltexprlem2  8661  ltexprlem3  8662  ltexprlem4  8663  ltexprlem6  8665  ltexprlem7  8666  prlem936  8671  eluzel2  10235  uzssz  10247  elixx3g  10669  ndmioo  10683  elfz2  10789  elfzoel1  10873  elfzoel2  10874  fzoval  10876  ltweuz  11024  fzofi  11036  sumz  12195  sumss  12197  znnen  12491  unbenlem  12955  prmreclem6  12968  eldmcoa  13897  efgsdm  15039  efgsval  15040  efgsp1  15046  efgsfo  15048  efgredleme  15052  efgred  15057  gexex  15145  torsubg  15146  dmdprd  15236  dprdval  15238  iocpnfordt  16945  icomnfordt  16946  uzrest  17592  qtopbaslem  18267  retopbas  18269  tgqioo  18306  re2ndc  18307  bndth  18456  tchcph  18667  ovolficcss  18829  ismbl  18885  uniiccdif  18933  dyadmbllem  18954  opnmbllem  18956  opnmblALT  18958  mbfimaopnlem  19010  itg1addlem4  19054  dvcmul  19293  dvcmulf  19294  dvexp  19302  c1liplem1  19343  deg1n0ima  19475  pserulm  19798  psercn2  19799  psercnlem2  19800  psercnlem1  19801  psercn  19802  pserdvlem1  19803  pserdvlem2  19804  pserdv  19805  pserdv2  19806  abelth  19817  efcn  19819  efcvx  19825  eff1olem  19910  dvrelog  19984  logf1o2  19997  dvlog  19998  efopn  20005  logtayl  20007  cxpcn3lem  20087  cxpcn3  20088  resqrcn  20089  atancl  20177  atanval  20180  dvatan  20231  atancn  20232  cnaddablo  21017  cnid  21018  addinv  21019  readdsubgo  21020  zaddsubgo  21021  ablomul  21022  mulid  21023  efghgrp  21040  cnrngo  21070  cncvc  21139  cnnv  21245  cnnvba  21247  cncph  21397  dfhnorm2  21701  hilablo  21739  hilid  21740  hilvc  21741  hhnv  21744  hhba  21746  hhph  21757  issh2  21788  hhssabloi  21839  hhssnv  21841  hhshsslem1  21844  imaelshi  22638  rnelshi  22639  nlelshi  22640  measbase  23528  erdszelem2  23723  erdszelem5  23726  erdszelem8  23729  bdaydm  24332  nZdef  25180  seff  27538  sblpnf  27539  dvsconst  27547  dvsid  27548  dvsef  27549  expgrowth  27552  addcomgi  27661
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-fn 5258  df-f 5259
  Copyright terms: Public domain W3C validator