Theorem fdmi 6657

Description: Inference associated with fdm 6654. 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 6654	. 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ dom 𝐹 = 𝐴

Syntax hints:   = wceq 1540  dom cdm 5614  ⟶wf 6469

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 206  df-an 397  df-fn 6476  df-f 6477

This theorem is referenced by:  f0cli  7024  rankvaln  9648  isnum2  9794  r0weon  9861  cfub  10098  cardcf  10101  cflecard  10102  cfle  10103  cflim2  10112  cfidm  10124  cardf  10399  smobeth  10435  inar1  10624  addcompq  10799  addcomnq  10800  mulcompq  10801  mulcomnq  10802  adderpq  10805  mulerpq  10806  addassnq  10807  mulassnq  10808  distrnq  10810  recmulnq  10813  recclnq  10815  dmrecnq  10817  lterpq  10819  ltanq  10820  ltmnq  10821  ltexnq  10824  nsmallnq  10826  ltbtwnnq  10827  prlem934  10882  ltaddpr  10883  ltexprlem2  10886  ltexprlem3  10887  ltexprlem4  10888  ltexprlem6  10890  ltexprlem7  10891  prlem936  10896  eluzel2  12680  uzssz  12696  elixx3g  13185  ndmioo  13199  elfz2  13339  fz0  13364  elfzoel1  13478  elfzoel2  13479  fzoval  13481  ltweuz  13774  fzofi  13787  dmhashres  14148  s1dm  14404  s2dm  14694  sumz  15525  sumss  15527  prod1  15745  prodss  15748  znnen  16012  unbenlem  16698  prmreclem6  16711  eldmcoa  17869  efgsdm  19423  efgsval  19424  efgsp1  19430  efgsfo  19432  efgredleme  19436  efgred  19441  gexex  19541  torsubg  19542  dmdprd  19688  dprdval  19693  iocpnfordt  22464  icomnfordt  22465  uzrest  23146  qtopbaslem  24020  retopbas  24022  tgqioo  24061  re2ndc  24062  bndth  24219  tcphcph  24499  ovolficcss  24731  ismbl  24788  uniiccdif  24840  dyadmbllem  24861  opnmbllem  24863  opnmblALT  24865  mbfimaopnlem  24917  itg1addlem4  24961  itg1addlem4OLD  24962  dvcmul  25206  dvcmulf  25207  dvexp  25215  c1liplem1  25258  deg1n0ima  25352  pserulm  25679  psercn2  25680  psercnlem2  25681  psercnlem1  25682  psercn  25683  pserdvlem1  25684  pserdvlem2  25685  pserdv  25686  pserdv2  25687  abelth  25698  efcn  25700  efcvx  25706  eff1olem  25802  dvrelog  25890  logf1o2  25903  dvlog  25904  efopn  25911  logtayl  25913  cxpcn3lem  25998  cxpcn3  25999  resqrtcn  26000  atancl  26129  atanval  26132  dvatan  26183  atancn  26184  bdaydm  27012  topnfbey  29062  cnaddabloOLD  29172  cnidOLD  29173  cncvcOLD  29174  cnnv  29268  cnnvba  29270  cncph  29410  dfhnorm2  29713  hilablo  29751  hilid  29752  hilvc  29753  hhnv  29756  hhba  29758  hhph  29769  issh2  29800  hhssabloi  29853  hhssnv  29855  hhshsslem1  29858  imaelshi  30649  rnelshi  30650  nlelshi  30651  xrofsup  31318  coinfliprv  32690  erdszelem2  33394  erdszelem5  33397  erdszelem8  33400  msrrcl  33745  mthmsta  33780  madess  34150  oldssmade  34151  madebdayim  34161  oldbdayim  34162  lrold  34168  icoreunrn  35628  icoreelrn  35630  relowlpssretop  35633  poimirlem26  35901  poimirlem27  35902  opnmbllem0  35911  dvtan  35925  fpwfvss  41329  seff  42237  sblpnf  42238  dvsconst  42258  dvsid  42259  dvsef  42260  expgrowth  42263  binomcxplemdvbinom  42281  binomcxplemdvsum  42283  binomcxplemnotnn0  42284  addcomgi  42384  dmuz  43094  dmico  43428  dvsinax  43779  fvvolioof  43855  fvvolicof  43857  dirkercncflem2  43970  fourierdlem42  44015  hoicvr  44412  ovolval3  44511