Theorem fdmi 6670

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

Syntax hints:   = wceq 1541  dom cdm 5621  ⟶wf 6485

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 6492  df-f 6493

This theorem is referenced by:  f0cli  7040  rankvaln  9702  isnum2  9848  r0weon  9913  cfub  10150  cardcf  10153  cflecard  10154  cfle  10155  cflim2  10164  cfidm  10176  cardf  10451  smobeth  10487  inar1  10676  addcompq  10851  addcomnq  10852  mulcompq  10853  mulcomnq  10854  adderpq  10857  mulerpq  10858  addassnq  10859  mulassnq  10860  distrnq  10862  recmulnq  10865  recclnq  10867  dmrecnq  10869  lterpq  10871  ltanq  10872  ltmnq  10873  ltexnq  10876  nsmallnq  10878  ltbtwnnq  10879  prlem934  10934  ltaddpr  10935  ltexprlem2  10938  ltexprlem3  10939  ltexprlem4  10940  ltexprlem6  10942  ltexprlem7  10943  prlem936  10948  eluzel2  12747  uzssz  12763  elixx3g  13268  ndmioo  13282  elfz2  13424  fz0  13449  elfzoel1  13567  elfzoel2  13568  fzoval  13570  ltweuz  13878  fzofi  13891  dmhashres  14258  s1dm  14526  s2dm  14807  sumz  15639  sumss  15641  prod1  15861  prodss  15864  znnen  16131  unbenlem  16830  prmreclem6  16843  eldmcoa  17982  efgsdm  19652  efgsval  19653  efgsp1  19659  efgsfo  19661  efgredleme  19665  efgred  19670  gexex  19775  torsubg  19776  dmdprd  19922  dprdval  19927  iocpnfordt  23140  icomnfordt  23141  uzrest  23822  qtopbaslem  24683  retopbas  24685  tgqioo  24725  re2ndc  24726  bndth  24894  tcphcph  25174  ovolficcss  25407  ismbl  25464  uniiccdif  25516  dyadmbllem  25537  opnmbllem  25539  opnmblALT  25541  mbfimaopnlem  25593  itg1addlem4  25637  dvcmul  25884  dvcmulf  25885  dvexp  25894  c1liplem1  25938  deg1n0ima  26031  pserulm  26368  psercn2  26369  psercn2OLD  26370  psercnlem2  26371  psercnlem1  26372  psercn  26373  pserdvlem1  26374  pserdvlem2  26375  pserdv  26376  pserdv2  26377  abelth  26388  efcn  26390  efcvx  26396  eff1olem  26494  dvrelog  26583  logf1o2  26596  dvlog  26597  efopn  26604  logtayl  26606  cxpcn3lem  26694  cxpcn3  26695  resqrtcn  26696  atancl  26828  atanval  26831  dvatan  26882  atancn  26883  bdaydm  27723  lltropt  27827  madess  27831  oldssmade  27832  oldss  27833  madebdayim  27843  oldbdayim  27844  lrold  27852  madefi  27868  oldfi  27869  topnfbey  30460  cnaddabloOLD  30572  cnidOLD  30573  cncvcOLD  30574  cnnv  30668  cnnvba  30670  cncph  30810  dfhnorm2  31113  hilablo  31151  hilid  31152  hilvc  31153  hhnv  31156  hhba  31158  hhph  31169  issh2  31200  hhssabloi  31253  hhssnv  31255  hhshsslem1  31258  imaelshi  32049  rnelshi  32050  nlelshi  32051  xrofsup  32761  ply1degltel  33566  ply1degleel  33567  ply1degltlss  33568  coinfliprv  34507  erdszelem2  35247  erdszelem5  35250  erdszelem8  35253  msrrcl  35598  mthmsta  35633  icoreunrn  37414  icoreelrn  37416  relowlpssretop  37419  poimirlem26  37696  poimirlem27  37697  opnmbllem0  37706  dvtan  37720  fpwfvss  43519  seff  44416  sblpnf  44417  dvsconst  44437  dvsid  44438  dvsef  44439  expgrowth  44442  binomcxplemdvbinom  44460  binomcxplemdvsum  44462  binomcxplemnotnn0  44463  addcomgi  44562  dmuz  45345  dmico  45677  dvsinax  46025  fvvolioof  46101  fvvolicof  46103  dirkercncflem2  46216  fourierdlem42  46261  hoicvr  46660  ovolval3  46759  sinnpoly  47005  fucofvalne  49440