Theorem fdmi 5726

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

Syntax hints:   = wceq 1383   dom cdm 4989   -->wf 5574

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 5581  df-f 5582

This theorem is referenced by:  f0cli  6027  rankvaln  8220  isnum2  8329  r0weon  8393  cfub  8632  cardcf  8635  cflecard  8636  cfle  8637  cflim2  8646  cfidm  8658  cardf  8928  smobeth  8964  inar1  9156  addcompq  9331  addcomnq  9332  mulcompq  9333  mulcomnq  9334  adderpq  9337  mulerpq  9338  addassnq  9339  mulassnq  9340  distrnq  9342  recmulnq  9345  recclnq  9347  dmrecnq  9349  lterpq  9351  ltanq  9352  ltmnq  9353  ltexnq  9356  nsmallnq  9358  ltbtwnnq  9359  prlem934  9414  ltaddpr  9415  ltexprlem2  9418  ltexprlem3  9419  ltexprlem4  9420  ltexprlem6  9422  ltexprlem7  9423  prlem936  9428  eluzel2  11097  uzssz  11111  elixx3g  11553  ndmioo  11567  elfz2  11690  fz0  11712  elfzoel1  11809  elfzoel2  11810  fzoval  11812  ltweuz  12054  fzofi  12066  dmhashres  12396  sumz  13526  sumss  13528  prod1  13733  prodss  13736  znnen  13928  unbenlem  14408  prmreclem6  14421  eldmcoa  15371  efgsdm  16727  efgsval  16728  efgsp1  16734  efgsfo  16736  efgredleme  16740  efgred  16745  gexex  16838  torsubg  16839  dmdprd  17008  dprdval  17013  dprdvalOLD  17015  iocpnfordt  19694  icomnfordt  19695  uzrest  20376  qtopbaslem  21243  retopbas  21245  tgqioo  21283  re2ndc  21284  bndth  21436  tchcph  21658  ovolficcss  21859  ismbl  21915  uniiccdif  21965  dyadmbllem  21986  opnmbllem  21988  opnmblALT  21990  mbfimaopnlem  22040  itg1addlem4  22084  dvcmul  22325  dvcmulf  22326  dvexp  22334  c1liplem1  22375  deg1n0ima  22467  pserulm  22795  psercn2  22796  psercnlem2  22797  psercnlem1  22798  psercn  22799  pserdvlem1  22800  pserdvlem2  22801  pserdv  22802  pserdv2  22803  abelth  22814  efcn  22816  efcvx  22822  eff1olem  22913  dvrelog  22996  logf1o2  23009  dvlog  23010  efopn  23017  logtayl  23019  cxpcn3lem  23099  cxpcn3  23100  resqrtcn  23101  atancl  23190  atanval  23193  dvatan  23244  atancn  23245  cnaddablo  25330  cnid  25331  addinv  25332  readdsubgo  25333  zaddsubgo  25334  ablomul  25335  mulid  25336  efghgrpOLD  25353  cnrngo  25383  cncvc  25454  cnnv  25560  cnnvba  25562  cncph  25712  dfhnorm2  26017  hilablo  26055  hilid  26056  hilvc  26057  hhnv  26060  hhba  26062  hhph  26073  issh2  26104  hhssabloi  26156  hhssnv  26158  hhshsslem1  26161  imaelshi  26955  rnelshi  26956  nlelshi  26957  xrofsup  27560  coinfliprv  28399  erdszelem2  28614  erdszelem5  28617  erdszelem8  28620  msrrcl  28881  mthmsta  28916  bdaydm  29414  opnmbllem0  30026  dvtan  30041  seff  31165  sblpnf  31166  dvsconst  31211  dvsid  31212  dvsef  31213  expgrowth  31216  addcomgi  31319  dvsinax  31662  dirkercncflem2  31840  fourierdlem42  31885