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

Theorem fdmi 5561
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 5560 . 2  |-  ( F : A --> B  ->  dom  F  =  A )
31, 2ax-mp 5 1  |-  dom  F  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1364   dom cdm 4836   -->wf 5411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-fn 5418  df-f 5419
This theorem is referenced by:  f0cli  5851  rankvaln  8002  isnum2  8111  r0weon  8175  cfub  8414  cardcf  8417  cflecard  8418  cfle  8419  cflim2  8428  cfidm  8440  cardf  8710  smobeth  8746  inar1  8938  addcompq  9115  addcomnq  9116  mulcompq  9117  mulcomnq  9118  adderpq  9121  mulerpq  9122  addassnq  9123  mulassnq  9124  distrnq  9126  recmulnq  9129  recclnq  9131  dmrecnq  9133  lterpq  9135  ltanq  9136  ltmnq  9137  ltexnq  9140  nsmallnq  9142  ltbtwnnq  9143  prlem934  9198  ltaddpr  9199  ltexprlem2  9202  ltexprlem3  9203  ltexprlem4  9204  ltexprlem6  9206  ltexprlem7  9207  prlem936  9212  eluzel2  10862  uzssz  10876  elixx3g  11309  ndmioo  11323  elfz2  11440  fz0  11461  elfzoel1  11547  elfzoel2  11548  fzoval  11550  ltweuz  11780  fzofi  11792  dmhashres  12108  sumz  13195  sumss  13197  znnen  13491  unbenlem  13965  prmreclem6  13978  eldmcoa  14929  efgsdm  16220  efgsval  16221  efgsp1  16227  efgsfo  16229  efgredleme  16233  efgred  16238  gexex  16328  torsubg  16329  dmdprd  16470  dprdval  16475  dprdvalOLD  16477  iocpnfordt  18778  icomnfordt  18779  uzrest  19429  qtopbaslem  20296  retopbas  20298  tgqioo  20336  re2ndc  20337  bndth  20489  tchcph  20711  ovolficcss  20912  ismbl  20968  uniiccdif  21017  dyadmbllem  21038  opnmbllem  21040  opnmblALT  21042  mbfimaopnlem  21092  itg1addlem4  21136  dvcmul  21377  dvcmulf  21378  dvexp  21386  c1liplem1  21427  deg1n0ima  21519  pserulm  21846  psercn2  21847  psercnlem2  21848  psercnlem1  21849  psercn  21850  pserdvlem1  21851  pserdvlem2  21852  pserdv  21853  pserdv2  21854  abelth  21865  efcn  21867  efcvx  21873  eff1olem  21963  dvrelog  22041  logf1o2  22054  dvlog  22055  efopn  22062  logtayl  22064  cxpcn3lem  22144  cxpcn3  22145  resqrcn  22146  atancl  22235  atanval  22238  dvatan  22289  atancn  22290  cnaddablo  23772  cnid  23773  addinv  23774  readdsubgo  23775  zaddsubgo  23776  ablomul  23777  mulid  23778  efghgrp  23795  cnrngo  23825  cncvc  23896  cnnv  24002  cnnvba  24004  cncph  24154  dfhnorm2  24459  hilablo  24497  hilid  24498  hilvc  24499  hhnv  24502  hhba  24504  hhph  24515  issh2  24546  hhssabloi  24598  hhssnv  24600  hhshsslem1  24603  imaelshi  25397  rnelshi  25398  nlelshi  25399  xrofsup  25988  coinfliprv  26795  erdszelem2  27010  erdszelem5  27013  erdszelem8  27016  prod1  27386  prodss  27389  bdaydm  27748  opnmbllem0  28352  dvtan  28367  seff  29520  sblpnf  29521  dvsconst  29529  dvsid  29530  dvsef  29531  expgrowth  29534  addcomgi  29637
  Copyright terms: Public domain W3C validator