Theorem fdmi 6717

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

Syntax hints:   = wceq 1568  dom cdm 5661  ⟶wf 6532

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 210  df-an 401  df-fn 6539  df-f 6540

This theorem is referenced by:  f0cli  7093  rankvaln  9770  isnum2  9930  r0weon  9995  cfub  10231  cardcf  10234  cflecard  10235  cfle  10236  cflim2  10246  cfidm  10258  cardf  10533  smobeth  10570  inar1  10759  addcompq  10934  addcomnq  10935  mulcompq  10936  mulcomnq  10937  adderpq  10940  mulerpq  10941  addassnq  10942  mulassnq  10943  distrnq  10945  recmulnq  10948  recclnq  10950  dmrecnq  10952  lterpq  10954  ltanq  10955  ltmnq  10956  ltexnq  10959  nsmallnq  10961  ltbtwnnq  10962  prlem934  11017  ltaddpr  11018  ltexprlem2  11021  ltexprlem3  11022  ltexprlem4  11023  ltexprlem6  11025  ltexprlem7  11026  prlem936  11031  eluzel2  12866  uzssz  12882  elixx3g  13384  ndmioo  13398  elfz2  13541  fz0  13566  elfzoel1  13685  elfzoel2  13686  fzoval  13688  ltweuz  13997  fzofi  14010  dmhashres  14377  s1dm  14646  s2dm  14927  sumz  15773  sumss  15775  prod1  15998  prodss  16001  znnen  16267  unbenlem  16967  prmreclem6  16980  eldmcoa  18121  efgsdm  19799  efgsval  19800  efgsp1  19806  efgsfo  19808  efgredleme  19812  efgred  19817  gexex  19922  torsubg  19923  dmdprd  20069  dprdval  20074  iocpnfordt  23351  icomnfordt  23352  uzrest  24033  qtopbaslem  24894  retopbas  24896  tgqioo  24936  re2ndc  24937  bndth  25096  tcphcph  25375  ovolficcss  25607  ismbl  25664  uniiccdif  25716  dyadmbllem  25737  opnmbllem  25739  opnmblALT  25741  mbfimaopnlem  25793  itg1addlem4  25837  dvcmul  26082  dvcmulf  26083  dvexp  26091  c1liplem1  26134  deg1n0ima  26225  pserulm  26561  psercn2  26562  psercnlem2  26563  psercnlem1  26564  psercn  26565  pserdvlem1  26566  pserdvlem2  26567  pserdv  26568  pserdv2  26569  abelth  26580  efcn  26582  efcvx  26588  eff1olem  26689  dvrelog  26778  logf1o2  26791  dvlog  26792  efopn  26799  logtayl  26801  cxpcn3lem  26888  cxpcn3  26889  resqrtcn  26890  atancl  27022  atanval  27025  dvatan  27076  atancn  27077  bdaydmOLD  27919  lltr  28031  madess  28035  oldssmade  28036  oldss  28039  madebdayim  28057  oldbdayim  28058  lrold  28066  madefi  28082  oldfi  28083  cutminmax  28105  oldfib  28546  topnfbey  30786  cnaddabloOLD  30899  cnidOLD  30900  cncvcOLD  30901  cnnv  30995  cnnvba  30997  cncph  31137  dfhnorm2  31440  hilablo  31478  hilid  31479  hilvc  31480  hhnv  31483  hhba  31485  hhph  31496  issh2  31527  hhssabloi  31580  hhssnv  31582  hhshsslem1  31585  imaelshi  32376  rnelshi  32377  nlelshi  32378  xrofsup  33078  ply1degltel  33850  ply1degleel  33851  ply1degltlss  33852  coinfliprv  34839  dfscott3  35478  erdszelem2  35650  erdszelem5  35653  erdszelem8  35656  msrrcl  36001  mthmsta  36036  icoreunrn  37971  icoreelrn  37973  relowlpssretop  37976  poimirlem26  38263  poimirlem27  38264  opnmbllem0  38273  dvtan  38287  fpwfvss  44108  seff  44989  sblpnf  44990  dvsconst  45010  dvsid  45011  dvsef  45012  expgrowth  45015  binomcxplemdvbinom  45033  binomcxplemdvsum  45035  binomcxplemnotnn0  45036  addcomgi  45134  dmuz  45919  dmico  46249  dvsinax  46597  fvvolioof  46673  fvvolicof  46675  dirkercncflem2  46788  fourierdlem42  46833  hoicvr  47232  ovolval3  47331  sinnpoly  47595  fucofvalne  50070