Theorem fdmi 5732

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 5731	. 2 |- ( F : A --> B -> dom F = A )
3	1, 2	ax-mp 5	1 |- dom F = A

Syntax hints:   = wceq 1443   dom cdm 4833   -->wf 5577

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 189  df-an 373  df-fn 5584  df-f 5585

This theorem is referenced by:  f0cli  6031  rankvaln  8267  isnum2  8376  r0weon  8440  cfub  8676  cardcf  8679  cflecard  8680  cfle  8681  cflim2  8690  cfidm  8702  cardf  8972  smobeth  9008  inar1  9197  addcompq  9372  addcomnq  9373  mulcompq  9374  mulcomnq  9375  adderpq  9378  mulerpq  9379  addassnq  9380  mulassnq  9381  distrnq  9383  recmulnq  9386  recclnq  9388  dmrecnq  9390  lterpq  9392  ltanq  9393  ltmnq  9394  ltexnq  9397  nsmallnq  9399  ltbtwnnq  9400  prlem934  9455  ltaddpr  9456  ltexprlem2  9459  ltexprlem3  9460  ltexprlem4  9461  ltexprlem6  9463  ltexprlem7  9464  prlem936  9469  eluzel2  11161  uzssz  11175  elixx3g  11645  ndmioo  11660  elfz2  11788  fz0  11811  elfzoel1  11915  elfzoel2  11916  fzoval  11918  ltweuz  12172  fzofi  12184  dmhashres  12521  sumz  13781  sumss  13783  prod1  13991  prodss  13994  znnen  14258  unbenlem  14845  prmreclem6  14858  eldmcoa  15953  efgsdm  17373  efgsval  17374  efgsp1  17380  efgsfo  17382  efgredleme  17386  efgred  17391  gexex  17484  torsubg  17485  dmdprd  17623  dprdval  17628  iocpnfordt  20224  icomnfordt  20225  uzrest  20905  qtopbaslem  21772  retopbas  21774  tgqioo  21811  re2ndc  21812  bndth  21979  tchcph  22204  ovolficcss  22415  ismbl  22473  uniiccdif  22528  dyadmbllem  22550  opnmbllem  22552  opnmblALT  22554  mbfimaopnlem  22604  itg1addlem4  22650  dvcmul  22891  dvcmulf  22892  dvexp  22900  c1liplem1  22941  deg1n0ima  23031  pserulm  23370  psercn2  23371  psercnlem2  23372  psercnlem1  23373  psercn  23374  pserdvlem1  23375  pserdvlem2  23376  pserdv  23377  pserdv2  23378  abelth  23389  efcn  23391  efcvx  23397  eff1olem  23490  dvrelog  23575  logf1o2  23588  dvlog  23589  efopn  23596  logtayl  23598  cxpcn3lem  23680  cxpcn3  23681  resqrtcn  23682  atancl  23800  atanval  23803  dvatan  23854  atancn  23855  topnfbey  25899  cnaddablo  26071  cnid  26072  addinv  26073  readdsubgo  26074  zaddsubgo  26075  ablomul  26076  mulid  26077  efghgrpOLD  26094  cnrngo  26124  cncvc  26195  cnnv  26301  cnnvba  26303  cncph  26453  dfhnorm2  26768  hilablo  26806  hilid  26807  hilvc  26808  hhnv  26811  hhba  26813  hhph  26824  issh2  26855  hhssabloi  26906  hhssnv  26908  hhshsslem1  26911  imaelshi  27704  rnelshi  27705  nlelshi  27706  xrofsup  28346  coinfliprv  29308  erdszelem2  29908  erdszelem5  29911  erdszelem8  29914  msrrcl  30174  mthmsta  30209  bdaydm  30560  icoreunrn  31755  icoreelrn  31757  relowlpssretop  31760  poimirlem26  31959  poimirlem27  31960  opnmbllem0  31969  dvtan  31985  seff  36651  sblpnf  36652  dvsconst  36673  dvsid  36674  dvsef  36675  expgrowth  36678  binomcxplemdvbinom  36696  binomcxplemdvsum  36698  binomcxplemnotnn0  36699  addcomgi  36803  dvsinax  37777  dirkercncflem2  37960  fourierdlem42  38006  fourierdlem42OLD  38007  hoicvr  38364