Theorem fdmi 6052

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

Syntax hints:   = wceq 1483   dom cdm 5114   -->wf 5884

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 197  df-an 386  df-fn 5891  df-f 5892

This theorem is referenced by:  f0cli  6370  rankvaln  8662  isnum2  8771  r0weon  8835  cfub  9071  cardcf  9074  cflecard  9075  cfle  9076  cflim2  9085  cfidm  9097  cardf  9372  smobeth  9408  inar1  9597  addcompq  9772  addcomnq  9773  mulcompq  9774  mulcomnq  9775  adderpq  9778  mulerpq  9779  addassnq  9780  mulassnq  9781  distrnq  9783  recmulnq  9786  recclnq  9788  dmrecnq  9790  lterpq  9792  ltanq  9793  ltmnq  9794  ltexnq  9797  nsmallnq  9799  ltbtwnnq  9800  prlem934  9855  ltaddpr  9856  ltexprlem2  9859  ltexprlem3  9860  ltexprlem4  9861  ltexprlem6  9863  ltexprlem7  9864  prlem936  9869  eluzel2  11692  uzssz  11707  elixx3g  12188  ndmioo  12202  elfz2  12333  fz0  12356  elfzoel1  12468  elfzoel2  12469  fzoval  12471  ltweuz  12760  fzofi  12773  dmhashres  13129  s1dm  13388  s2dm  13635  sumz  14453  sumss  14455  prod1  14674  prodss  14677  znnen  14941  unbenlem  15612  prmreclem6  15625  eldmcoa  16715  efgsdm  18143  efgsval  18144  efgsp1  18150  efgsfo  18152  efgredleme  18156  efgred  18161  gexex  18256  torsubg  18257  dmdprd  18397  dprdval  18402  iocpnfordt  21019  icomnfordt  21020  uzrest  21701  qtopbaslem  22562  retopbas  22564  tgqioo  22603  re2ndc  22604  bndth  22757  tchcph  23036  ovolficcss  23238  ismbl  23294  uniiccdif  23346  dyadmbllem  23367  opnmbllem  23369  opnmblALT  23371  mbfimaopnlem  23422  itg1addlem4  23466  dvcmul  23707  dvcmulf  23708  dvexp  23716  c1liplem1  23759  deg1n0ima  23849  pserulm  24176  psercn2  24177  psercnlem2  24178  psercnlem1  24179  psercn  24180  pserdvlem1  24181  pserdvlem2  24182  pserdv  24183  pserdv2  24184  abelth  24195  efcn  24197  efcvx  24203  eff1olem  24294  dvrelog  24383  logf1o2  24396  dvlog  24397  efopn  24404  logtayl  24406  cxpcn3lem  24488  cxpcn3  24489  resqrtcn  24490  atancl  24608  atanval  24611  dvatan  24662  atancn  24663  topnfbey  27325  cnaddabloOLD  27436  cnidOLD  27437  cncvcOLD  27438  cnnv  27532  cnnvba  27534  cncph  27674  dfhnorm2  27979  hilablo  28017  hilid  28018  hilvc  28019  hhnv  28022  hhba  28024  hhph  28035  issh2  28066  hhssabloi  28119  hhssnv  28121  hhshsslem1  28124  imaelshi  28917  rnelshi  28918  nlelshi  28919  xrofsup  29533  coinfliprv  30544  erdszelem2  31174  erdszelem5  31177  erdszelem8  31180  msrrcl  31440  mthmsta  31475  bdaydm  31890  icoreunrn  33207  icoreelrn  33209  relowlpssretop  33212  poimirlem26  33435  poimirlem27  33436  opnmbllem0  33445  dvtan  33460  seff  38508  sblpnf  38509  dvsconst  38529  dvsid  38530  dvsef  38531  expgrowth  38534  binomcxplemdvbinom  38552  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  addcomgi  38660  dmuz  39440  dmico  39792  dvsinax  40127  fvvolioof  40206  fvvolicof  40208  dirkercncflem2  40321  fourierdlem42  40366  hoicvr  40762  ovolval3  40861