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

Theorem fdmi 5588
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 5587 . 2  |-  ( F : A --> B  ->  dom  F  =  A )
31, 2ax-mp 8 1  |-  dom  F  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1652   dom cdm 4870   -->wf 5442
This theorem is referenced by:  f0cli  5872  rankvaln  7715  isnum2  7822  r0weon  7884  cfub  8119  cardcf  8122  cflecard  8123  cfle  8124  cflim2  8133  cfidm  8145  cardf  8415  smobeth  8451  inar1  8640  addcompq  8817  addcomnq  8818  mulcompq  8819  mulcomnq  8820  adderpq  8823  mulerpq  8824  addassnq  8825  mulassnq  8826  distrnq  8828  recmulnq  8831  recclnq  8833  dmrecnq  8835  lterpq  8837  ltanq  8838  ltmnq  8839  ltexnq  8842  nsmallnq  8844  ltbtwnnq  8845  prlem934  8900  ltaddpr  8901  ltexprlem2  8904  ltexprlem3  8905  ltexprlem4  8906  ltexprlem6  8908  ltexprlem7  8909  prlem936  8914  eluzel2  10483  uzssz  10495  elixx3g  10919  ndmioo  10933  elfz2  11040  elfzoel1  11128  elfzoel2  11129  fzoval  11131  ltweuz  11291  fzofi  11303  sumz  12506  sumss  12508  znnen  12802  unbenlem  13266  prmreclem6  13279  eldmcoa  14210  efgsdm  15352  efgsval  15353  efgsp1  15359  efgsfo  15361  efgredleme  15365  efgred  15370  gexex  15458  torsubg  15459  dmdprd  15549  dprdval  15551  iocpnfordt  17269  icomnfordt  17270  uzrest  17919  qtopbaslem  18782  retopbas  18784  tgqioo  18821  re2ndc  18822  bndth  18973  tchcph  19184  ovolficcss  19356  ismbl  19412  uniiccdif  19460  dyadmbllem  19481  opnmbllem  19483  opnmblALT  19485  mbfimaopnlem  19537  itg1addlem4  19581  dvcmul  19820  dvcmulf  19821  dvexp  19829  c1liplem1  19870  deg1n0ima  20002  pserulm  20328  psercn2  20329  psercnlem2  20330  psercnlem1  20331  psercn  20332  pserdvlem1  20333  pserdvlem2  20334  pserdv  20335  pserdv2  20336  abelth  20347  efcn  20349  efcvx  20355  eff1olem  20440  dvrelog  20518  logf1o2  20531  dvlog  20532  efopn  20539  logtayl  20541  cxpcn3lem  20621  cxpcn3  20622  resqrcn  20623  atancl  20711  atanval  20714  dvatan  20765  atancn  20766  cnaddablo  21928  cnid  21929  addinv  21930  readdsubgo  21931  zaddsubgo  21932  ablomul  21933  mulid  21934  efghgrp  21951  cnrngo  21981  cncvc  22052  cnnv  22158  cnnvba  22160  cncph  22310  dfhnorm2  22614  hilablo  22652  hilid  22653  hilvc  22654  hhnv  22657  hhba  22659  hhph  22670  issh2  22701  hhssabloi  22752  hhssnv  22754  hhshsslem1  22757  imaelshi  23551  rnelshi  23552  nlelshi  23553  xrofsup  24116  dmhashres  24147  coinfliprv  24730  erdszelem2  24868  erdszelem5  24871  erdszelem8  24874  prod1  25260  prodss  25263  bdaydm  25598  mblfinlem  26207  seff  27470  sblpnf  27471  dvsconst  27479  dvsid  27480  dvsef  27481  expgrowth  27484  addcomgi  27592
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 178  df-an 361  df-fn 5449  df-f 5450
  Copyright terms: Public domain W3C validator