Theorem fdmi 6674

Description: Inference associated with fdm 6672. The domain of a mapping. (Contributed by NM, 28-Jul-2008.)

Hypothesis

Ref	Expression
fdmi.1	⊢ 𝐹:𝐴⟶𝐵

Assertion

Ref	Expression
fdmi	⊢ dom 𝐹 = 𝐴

Proof of Theorem fdmi

Step	Hyp	Ref	Expression
1		fdmi.1	. 2 ⊢ 𝐹:𝐴⟶𝐵
2		fdm 6672	. 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ dom 𝐹 = 𝐴

Syntax hints:   = wceq 1542  dom cdm 5625  ⟶wf 6489

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 207  df-an 396  df-fn 6496  df-f 6497

This theorem is referenced by:  f0cli  7045  rankvaln  9715  isnum2  9861  r0weon  9926  cfub  10163  cardcf  10166  cflecard  10167  cfle  10168  cflim2  10177  cfidm  10189  cardf  10464  smobeth  10501  inar1  10690  addcompq  10865  addcomnq  10866  mulcompq  10867  mulcomnq  10868  adderpq  10871  mulerpq  10872  addassnq  10873  mulassnq  10874  distrnq  10876  recmulnq  10879  recclnq  10881  dmrecnq  10883  lterpq  10885  ltanq  10886  ltmnq  10887  ltexnq  10890  nsmallnq  10892  ltbtwnnq  10893  prlem934  10948  ltaddpr  10949  ltexprlem2  10952  ltexprlem3  10953  ltexprlem4  10954  ltexprlem6  10956  ltexprlem7  10957  prlem936  10962  eluzel2  12760  uzssz  12776  elixx3g  13278  ndmioo  13292  elfz2  13434  fz0  13459  elfzoel1  13577  elfzoel2  13578  fzoval  13580  ltweuz  13888  fzofi  13901  dmhashres  14268  s1dm  14536  s2dm  14817  sumz  15649  sumss  15651  prod1  15871  prodss  15874  znnen  16141  unbenlem  16840  prmreclem6  16853  eldmcoa  17993  efgsdm  19663  efgsval  19664  efgsp1  19670  efgsfo  19672  efgredleme  19676  efgred  19681  gexex  19786  torsubg  19787  dmdprd  19933  dprdval  19938  iocpnfordt  23163  icomnfordt  23164  uzrest  23845  qtopbaslem  24706  retopbas  24708  tgqioo  24748  re2ndc  24749  bndth  24917  tcphcph  25197  ovolficcss  25430  ismbl  25487  uniiccdif  25539  dyadmbllem  25560  opnmbllem  25562  opnmblALT  25564  mbfimaopnlem  25616  itg1addlem4  25660  dvcmul  25907  dvcmulf  25908  dvexp  25917  c1liplem1  25961  deg1n0ima  26054  pserulm  26391  psercn2  26392  psercn2OLD  26393  psercnlem2  26394  psercnlem1  26395  psercn  26396  pserdvlem1  26397  pserdvlem2  26398  pserdv  26399  pserdv2  26400  abelth  26411  efcn  26413  efcvx  26419  eff1olem  26517  dvrelog  26606  logf1o2  26619  dvlog  26620  efopn  26627  logtayl  26629  cxpcn3lem  26717  cxpcn3  26718  resqrtcn  26719  atancl  26851  atanval  26854  dvatan  26905  atancn  26906  bdaydm  27750  lltropt  27854  madess  27858  oldssmade  27859  oldss  27860  madebdayim  27870  oldbdayim  27871  lrold  27879  madefi  27895  oldfi  27896  cutminmax  27918  oldfib  28356  topnfbey  30527  cnaddabloOLD  30639  cnidOLD  30640  cncvcOLD  30641  cnnv  30735  cnnvba  30737  cncph  30877  dfhnorm2  31180  hilablo  31218  hilid  31219  hilvc  31220  hhnv  31223  hhba  31225  hhph  31236  issh2  31267  hhssabloi  31320  hhssnv  31322  hhshsslem1  31325  imaelshi  32116  rnelshi  32117  nlelshi  32118  xrofsup  32828  ply1degltel  33656  ply1degleel  33657  ply1degltlss  33658  coinfliprv  34621  erdszelem2  35367  erdszelem5  35370  erdszelem8  35373  msrrcl  35718  mthmsta  35753  icoreunrn  37535  icoreelrn  37537  relowlpssretop  37540  poimirlem26  37818  poimirlem27  37819  opnmbllem0  37828  dvtan  37842  fpwfvss  43689  seff  44586  sblpnf  44587  dvsconst  44607  dvsid  44608  dvsef  44609  expgrowth  44612  binomcxplemdvbinom  44630  binomcxplemdvsum  44632  binomcxplemnotnn0  44633  addcomgi  44732  dmuz  45514  dmico  45845  dvsinax  46193  fvvolioof  46269  fvvolicof  46271  dirkercncflem2  46384  fourierdlem42  46429  hoicvr  46828  ovolval3  46927  sinnpoly  47173  fucofvalne  49606