Theorem fdmi 5555

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

Syntax hints:   = wceq 1649   dom cdm 4837   -->wf 5409

This theorem is referenced by:  f0cli  5839  rankvaln  7681  isnum2  7788  r0weon  7850  cfub  8085  cardcf  8088  cflecard  8089  cfle  8090  cflim2  8099  cfidm  8111  cardf  8381  smobeth  8417  inar1  8606  addcompq  8783  addcomnq  8784  mulcompq  8785  mulcomnq  8786  adderpq  8789  mulerpq  8790  addassnq  8791  mulassnq  8792  distrnq  8794  recmulnq  8797  recclnq  8799  dmrecnq  8801  lterpq  8803  ltanq  8804  ltmnq  8805  ltexnq  8808  nsmallnq  8810  ltbtwnnq  8811  prlem934  8866  ltaddpr  8867  ltexprlem2  8870  ltexprlem3  8871  ltexprlem4  8872  ltexprlem6  8874  ltexprlem7  8875  prlem936  8880  eluzel2  10449  uzssz  10461  elixx3g  10885  ndmioo  10899  elfz2  11006  elfzoel1  11093  elfzoel2  11094  fzoval  11096  ltweuz  11256  fzofi  11268  sumz  12471  sumss  12473  znnen  12767  unbenlem  13231  prmreclem6  13244  eldmcoa  14175  efgsdm  15317  efgsval  15318  efgsp1  15324  efgsfo  15326  efgredleme  15330  efgred  15335  gexex  15423  torsubg  15424  dmdprd  15514  dprdval  15516  iocpnfordt  17233  icomnfordt  17234  uzrest  17882  qtopbaslem  18745  retopbas  18747  tgqioo  18784  re2ndc  18785  bndth  18936  tchcph  19147  ovolficcss  19319  ismbl  19375  uniiccdif  19423  dyadmbllem  19444  opnmbllem  19446  opnmblALT  19448  mbfimaopnlem  19500  itg1addlem4  19544  dvcmul  19783  dvcmulf  19784  dvexp  19792  c1liplem1  19833  deg1n0ima  19965  pserulm  20291  psercn2  20292  psercnlem2  20293  psercnlem1  20294  psercn  20295  pserdvlem1  20296  pserdvlem2  20297  pserdv  20298  pserdv2  20299  abelth  20310  efcn  20312  efcvx  20318  eff1olem  20403  dvrelog  20481  logf1o2  20494  dvlog  20495  efopn  20502  logtayl  20504  cxpcn3lem  20584  cxpcn3  20585  resqrcn  20586  atancl  20674  atanval  20677  dvatan  20728  atancn  20729  cnaddablo  21891  cnid  21892  addinv  21893  readdsubgo  21894  zaddsubgo  21895  ablomul  21896  mulid  21897  efghgrp  21914  cnrngo  21944  cncvc  22015  cnnv  22121  cnnvba  22123  cncph  22273  dfhnorm2  22577  hilablo  22615  hilid  22616  hilvc  22617  hhnv  22620  hhba  22622  hhph  22633  issh2  22664  hhssabloi  22715  hhssnv  22717  hhshsslem1  22720  imaelshi  23514  rnelshi  23515  nlelshi  23516  xrofsup  24079  dmhashres  24110  coinfliprv  24693  erdszelem2  24831  erdszelem5  24834  erdszelem8  24837  prod1  25223  prodss  25226  bdaydm  25546  mblfinlem  26143  seff  27406  sblpnf  27407  dvsconst  27415  dvsid  27416  dvsef  27417  expgrowth  27420  addcomgi  27528

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 5416  df-f 5417