Theorem fdmi 6621

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

Syntax hints:   = wceq 1539  dom cdm 5590  ⟶wf 6433

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 6440  df-f 6441

This theorem is referenced by:  f0cli  6983  rankvaln  9566  isnum2  9712  r0weon  9777  cfub  10014  cardcf  10017  cflecard  10018  cfle  10019  cflim2  10028  cfidm  10040  cardf  10315  smobeth  10351  inar1  10540  addcompq  10715  addcomnq  10716  mulcompq  10717  mulcomnq  10718  adderpq  10721  mulerpq  10722  addassnq  10723  mulassnq  10724  distrnq  10726  recmulnq  10729  recclnq  10731  dmrecnq  10733  lterpq  10735  ltanq  10736  ltmnq  10737  ltexnq  10740  nsmallnq  10742  ltbtwnnq  10743  prlem934  10798  ltaddpr  10799  ltexprlem2  10802  ltexprlem3  10803  ltexprlem4  10804  ltexprlem6  10806  ltexprlem7  10807  prlem936  10812  eluzel2  12596  uzssz  12612  elixx3g  13101  ndmioo  13115  elfz2  13255  fz0  13280  elfzoel1  13394  elfzoel2  13395  fzoval  13397  ltweuz  13690  fzofi  13703  dmhashres  14064  s1dm  14322  s2dm  14612  sumz  15443  sumss  15445  prod1  15663  prodss  15666  znnen  15930  unbenlem  16618  prmreclem6  16631  eldmcoa  17789  efgsdm  19345  efgsval  19346  efgsp1  19352  efgsfo  19354  efgredleme  19358  efgred  19363  gexex  19463  torsubg  19464  dmdprd  19610  dprdval  19615  iocpnfordt  22375  icomnfordt  22376  uzrest  23057  qtopbaslem  23931  retopbas  23933  tgqioo  23972  re2ndc  23973  bndth  24130  tcphcph  24410  ovolficcss  24642  ismbl  24699  uniiccdif  24751  dyadmbllem  24772  opnmbllem  24774  opnmblALT  24776  mbfimaopnlem  24828  itg1addlem4  24872  itg1addlem4OLD  24873  dvcmul  25117  dvcmulf  25118  dvexp  25126  c1liplem1  25169  deg1n0ima  25263  pserulm  25590  psercn2  25591  psercnlem2  25592  psercnlem1  25593  psercn  25594  pserdvlem1  25595  pserdvlem2  25596  pserdv  25597  pserdv2  25598  abelth  25609  efcn  25611  efcvx  25617  eff1olem  25713  dvrelog  25801  logf1o2  25814  dvlog  25815  efopn  25822  logtayl  25824  cxpcn3lem  25909  cxpcn3  25910  resqrtcn  25911  atancl  26040  atanval  26043  dvatan  26094  atancn  26095  topnfbey  28842  cnaddabloOLD  28952  cnidOLD  28953  cncvcOLD  28954  cnnv  29048  cnnvba  29050  cncph  29190  dfhnorm2  29493  hilablo  29531  hilid  29532  hilvc  29533  hhnv  29536  hhba  29538  hhph  29549  issh2  29580  hhssabloi  29633  hhssnv  29635  hhshsslem1  29638  imaelshi  30429  rnelshi  30430  nlelshi  30431  xrofsup  31099  coinfliprv  32458  erdszelem2  33163  erdszelem5  33166  erdszelem8  33169  msrrcl  33514  mthmsta  33549  bdaydm  33978  madess  34068  oldssmade  34069  madebdayim  34079  oldbdayim  34080  lrold  34086  icoreunrn  35539  icoreelrn  35541  relowlpssretop  35544  poimirlem26  35812  poimirlem27  35813  opnmbllem0  35822  dvtan  35836  seff  41934  sblpnf  41935  dvsconst  41955  dvsid  41956  dvsef  41957  expgrowth  41960  binomcxplemdvbinom  41978  binomcxplemdvsum  41980  binomcxplemnotnn0  41981  addcomgi  42081  dmuz  42784  dmico  43110  dvsinax  43461  fvvolioof  43537  fvvolicof  43539  dirkercncflem2  43652  fourierdlem42  43697  hoicvr  44093  ovolval3  44192