Theorem fdmi 5742

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

Syntax hints:   = wceq 1437   dom cdm 4845   -->wf 5588

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 188  df-an 372  df-fn 5595  df-f 5596

This theorem is referenced by:  f0cli  6039  rankvaln  8260  isnum2  8369  r0weon  8433  cfub  8668  cardcf  8671  cflecard  8672  cfle  8673  cflim2  8682  cfidm  8694  cardf  8964  smobeth  9000  inar1  9189  addcompq  9364  addcomnq  9365  mulcompq  9366  mulcomnq  9367  adderpq  9370  mulerpq  9371  addassnq  9372  mulassnq  9373  distrnq  9375  recmulnq  9378  recclnq  9380  dmrecnq  9382  lterpq  9384  ltanq  9385  ltmnq  9386  ltexnq  9389  nsmallnq  9391  ltbtwnnq  9392  prlem934  9447  ltaddpr  9448  ltexprlem2  9451  ltexprlem3  9452  ltexprlem4  9453  ltexprlem6  9455  ltexprlem7  9456  prlem936  9461  eluzel2  11153  uzssz  11167  elixx3g  11637  ndmioo  11652  elfz2  11778  fz0  11801  elfzoel1  11905  elfzoel2  11906  fzoval  11908  ltweuz  12161  fzofi  12173  dmhashres  12510  sumz  13755  sumss  13757  prod1  13965  prodss  13968  znnen  14232  unbenlem  14804  prmreclem6  14817  eldmcoa  15904  efgsdm  17308  efgsval  17309  efgsp1  17315  efgsfo  17317  efgredleme  17321  efgred  17326  gexex  17419  torsubg  17420  dmdprd  17558  dprdval  17563  iocpnfordt  20155  icomnfordt  20156  uzrest  20836  qtopbaslem  21683  retopbas  21685  tgqioo  21722  re2ndc  21723  bndth  21875  tchcph  22097  ovolficcss  22296  ismbl  22354  uniiccdif  22409  dyadmbllem  22431  opnmbllem  22433  opnmblALT  22435  mbfimaopnlem  22485  itg1addlem4  22531  dvcmul  22772  dvcmulf  22773  dvexp  22781  c1liplem1  22822  deg1n0ima  22912  pserulm  23239  psercn2  23240  psercnlem2  23241  psercnlem1  23242  psercn  23243  pserdvlem1  23244  pserdvlem2  23245  pserdv  23246  pserdv2  23247  abelth  23258  efcn  23260  efcvx  23266  eff1olem  23359  dvrelog  23444  logf1o2  23457  dvlog  23458  efopn  23465  logtayl  23467  cxpcn3lem  23549  cxpcn3  23550  resqrtcn  23551  atancl  23669  atanval  23672  dvatan  23723  atancn  23724  topnfbey  25748  cnaddablo  25920  cnid  25921  addinv  25922  readdsubgo  25923  zaddsubgo  25924  ablomul  25925  mulid  25926  efghgrpOLD  25943  cnrngo  25973  cncvc  26044  cnnv  26150  cnnvba  26152  cncph  26302  dfhnorm2  26607  hilablo  26645  hilid  26646  hilvc  26647  hhnv  26650  hhba  26652  hhph  26663  issh2  26694  hhssabloi  26745  hhssnv  26747  hhshsslem1  26750  imaelshi  27543  rnelshi  27544  nlelshi  27545  xrofsup  28186  coinfliprv  29138  erdszelem2  29700  erdszelem5  29703  erdszelem8  29706  msrrcl  29966  mthmsta  30001  bdaydm  30349  icoreunrn  31493  icoreelrn  31495  relowlpssretop  31498  poimirlem26  31670  poimirlem27  31671  opnmbllem0  31680  dvtan  31696  seff  36298  sblpnf  36299  dvsconst  36320  dvsid  36321  dvsef  36322  expgrowth  36325  binomcxplemdvbinom  36343  binomcxplemdvsum  36345  binomcxplemnotnn0  36346  addcomgi  36450  dvsinax  37359  dirkercncflem2  37539  fourierdlem42  37584