Theorem fdmi 5735

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

Syntax hints:   = wceq 1379   dom cdm 4999   -->wf 5583

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 5590  df-f 5591

This theorem is referenced by:  f0cli  6031  rankvaln  8216  isnum2  8325  r0weon  8389  cfub  8628  cardcf  8631  cflecard  8632  cfle  8633  cflim2  8642  cfidm  8654  cardf  8924  smobeth  8960  inar1  9152  addcompq  9327  addcomnq  9328  mulcompq  9329  mulcomnq  9330  adderpq  9333  mulerpq  9334  addassnq  9335  mulassnq  9336  distrnq  9338  recmulnq  9341  recclnq  9343  dmrecnq  9345  lterpq  9347  ltanq  9348  ltmnq  9349  ltexnq  9352  nsmallnq  9354  ltbtwnnq  9355  prlem934  9410  ltaddpr  9411  ltexprlem2  9414  ltexprlem3  9415  ltexprlem4  9416  ltexprlem6  9418  ltexprlem7  9419  prlem936  9424  eluzel2  11086  uzssz  11100  elixx3g  11541  ndmioo  11555  elfz2  11678  fz0  11700  elfzoel1  11794  elfzoel2  11795  fzoval  11797  ltweuz  12039  fzofi  12051  dmhashres  12381  sumz  13506  sumss  13508  znnen  13806  unbenlem  14284  prmreclem6  14297  eldmcoa  15249  efgsdm  16551  efgsval  16552  efgsp1  16558  efgsfo  16560  efgredleme  16564  efgred  16569  gexex  16659  torsubg  16660  dmdprd  16829  dprdval  16834  dprdvalOLD  16836  iocpnfordt  19498  icomnfordt  19499  uzrest  20149  qtopbaslem  21016  retopbas  21018  tgqioo  21056  re2ndc  21057  bndth  21209  tchcph  21431  ovolficcss  21632  ismbl  21688  uniiccdif  21738  dyadmbllem  21759  opnmbllem  21761  opnmblALT  21763  mbfimaopnlem  21813  itg1addlem4  21857  dvcmul  22098  dvcmulf  22099  dvexp  22107  c1liplem1  22148  deg1n0ima  22240  pserulm  22567  psercn2  22568  psercnlem2  22569  psercnlem1  22570  psercn  22571  pserdvlem1  22572  pserdvlem2  22573  pserdv  22574  pserdv2  22575  abelth  22586  efcn  22588  efcvx  22594  eff1olem  22684  dvrelog  22762  logf1o2  22775  dvlog  22776  efopn  22783  logtayl  22785  cxpcn3lem  22865  cxpcn3  22866  resqrtcn  22867  atancl  22956  atanval  22959  dvatan  23010  atancn  23011  cnaddablo  25044  cnid  25045  addinv  25046  readdsubgo  25047  zaddsubgo  25048  ablomul  25049  mulid  25050  efghgrp  25067  cnrngo  25097  cncvc  25168  cnnv  25274  cnnvba  25276  cncph  25426  dfhnorm2  25731  hilablo  25769  hilid  25770  hilvc  25771  hhnv  25774  hhba  25776  hhph  25787  issh2  25818  hhssabloi  25870  hhssnv  25872  hhshsslem1  25875  imaelshi  26669  rnelshi  26670  nlelshi  26671  xrofsup  27266  coinfliprv  28077  erdszelem2  28292  erdszelem5  28295  erdszelem8  28298  prod1  28669  prodss  28672  bdaydm  29031  opnmbllem0  29643  dvtan  29658  seff  30808  sblpnf  30809  dvsconst  30851  dvsid  30852  dvsef  30853  expgrowth  30856  addcomgi  30959  dvsinax  31257  dirkercncflem2  31420  fourierdlem42  31465