Theorem fdmi 5576

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

Step	Hyp	Ref	Expression
1		fdmi.1	. 2 |- F : A --> B
2		fdm 5575	. 2 |- ( F : A --> B -> dom F = A )
3	1, 2	ax-mp 5	1 |- dom F = A

Syntax hints:   = wceq 1369   dom cdm 4852   -->wf 5426

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 5433  df-f 5434

This theorem is referenced by:  f0cli  5866  rankvaln  8018  isnum2  8127  r0weon  8191  cfub  8430  cardcf  8433  cflecard  8434  cfle  8435  cflim2  8444  cfidm  8456  cardf  8726  smobeth  8762  inar1  8954  addcompq  9131  addcomnq  9132  mulcompq  9133  mulcomnq  9134  adderpq  9137  mulerpq  9138  addassnq  9139  mulassnq  9140  distrnq  9142  recmulnq  9145  recclnq  9147  dmrecnq  9149  lterpq  9151  ltanq  9152  ltmnq  9153  ltexnq  9156  nsmallnq  9158  ltbtwnnq  9159  prlem934  9214  ltaddpr  9215  ltexprlem2  9218  ltexprlem3  9219  ltexprlem4  9220  ltexprlem6  9222  ltexprlem7  9223  prlem936  9228  eluzel2  10878  uzssz  10892  elixx3g  11325  ndmioo  11339  elfz2  11456  fz0  11477  elfzoel1  11563  elfzoel2  11564  fzoval  11566  ltweuz  11796  fzofi  11808  dmhashres  12124  sumz  13211  sumss  13213  znnen  13507  unbenlem  13981  prmreclem6  13994  eldmcoa  14945  efgsdm  16239  efgsval  16240  efgsp1  16246  efgsfo  16248  efgredleme  16252  efgred  16257  gexex  16347  torsubg  16348  dmdprd  16492  dprdval  16497  dprdvalOLD  16499  iocpnfordt  18831  icomnfordt  18832  uzrest  19482  qtopbaslem  20349  retopbas  20351  tgqioo  20389  re2ndc  20390  bndth  20542  tchcph  20764  ovolficcss  20965  ismbl  21021  uniiccdif  21070  dyadmbllem  21091  opnmbllem  21093  opnmblALT  21095  mbfimaopnlem  21145  itg1addlem4  21189  dvcmul  21430  dvcmulf  21431  dvexp  21439  c1liplem1  21480  deg1n0ima  21572  pserulm  21899  psercn2  21900  psercnlem2  21901  psercnlem1  21902  psercn  21903  pserdvlem1  21904  pserdvlem2  21905  pserdv  21906  pserdv2  21907  abelth  21918  efcn  21920  efcvx  21926  eff1olem  22016  dvrelog  22094  logf1o2  22107  dvlog  22108  efopn  22115  logtayl  22117  cxpcn3lem  22197  cxpcn3  22198  resqrcn  22199  atancl  22288  atanval  22291  dvatan  22342  atancn  22343  cnaddablo  23849  cnid  23850  addinv  23851  readdsubgo  23852  zaddsubgo  23853  ablomul  23854  mulid  23855  efghgrp  23872  cnrngo  23902  cncvc  23973  cnnv  24079  cnnvba  24081  cncph  24231  dfhnorm2  24536  hilablo  24574  hilid  24575  hilvc  24576  hhnv  24579  hhba  24581  hhph  24592  issh2  24623  hhssabloi  24675  hhssnv  24677  hhshsslem1  24680  imaelshi  25474  rnelshi  25475  nlelshi  25476  xrofsup  26067  coinfliprv  26877  erdszelem2  27092  erdszelem5  27095  erdszelem8  27098  prod1  27469  prodss  27472  bdaydm  27831  opnmbllem0  28439  dvtan  28454  seff  29607  sblpnf  29608  dvsconst  29616  dvsid  29617  dvsef  29618  expgrowth  29621  addcomgi  29724