Theorem fdmi 6729

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

Syntax hints:   = wceq 1541  dom cdm 5676  ⟶wf 6539

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 6546  df-f 6547

This theorem is referenced by:  f0cli  7099  rankvaln  9793  isnum2  9939  r0weon  10006  cfub  10243  cardcf  10246  cflecard  10247  cfle  10248  cflim2  10257  cfidm  10269  cardf  10544  smobeth  10580  inar1  10769  addcompq  10944  addcomnq  10945  mulcompq  10946  mulcomnq  10947  adderpq  10950  mulerpq  10951  addassnq  10952  mulassnq  10953  distrnq  10955  recmulnq  10958  recclnq  10960  dmrecnq  10962  lterpq  10964  ltanq  10965  ltmnq  10966  ltexnq  10969  nsmallnq  10971  ltbtwnnq  10972  prlem934  11027  ltaddpr  11028  ltexprlem2  11031  ltexprlem3  11032  ltexprlem4  11033  ltexprlem6  11035  ltexprlem7  11036  prlem936  11041  eluzel2  12826  uzssz  12842  elixx3g  13336  ndmioo  13350  elfz2  13490  fz0  13515  elfzoel1  13629  elfzoel2  13630  fzoval  13632  ltweuz  13925  fzofi  13938  dmhashres  14300  s1dm  14557  s2dm  14840  sumz  15667  sumss  15669  prod1  15887  prodss  15890  znnen  16154  unbenlem  16840  prmreclem6  16853  eldmcoa  18014  efgsdm  19597  efgsval  19598  efgsp1  19604  efgsfo  19606  efgredleme  19610  efgred  19615  gexex  19720  torsubg  19721  dmdprd  19867  dprdval  19872  iocpnfordt  22718  icomnfordt  22719  uzrest  23400  qtopbaslem  24274  retopbas  24276  tgqioo  24315  re2ndc  24316  bndth  24473  tcphcph  24753  ovolficcss  24985  ismbl  25042  uniiccdif  25094  dyadmbllem  25115  opnmbllem  25117  opnmblALT  25119  mbfimaopnlem  25171  itg1addlem4  25215  itg1addlem4OLD  25216  dvcmul  25460  dvcmulf  25461  dvexp  25469  c1liplem1  25512  deg1n0ima  25606  pserulm  25933  psercn2  25934  psercnlem2  25935  psercnlem1  25936  psercn  25937  pserdvlem1  25938  pserdvlem2  25939  pserdv  25940  pserdv2  25941  abelth  25952  efcn  25954  efcvx  25960  eff1olem  26056  dvrelog  26144  logf1o2  26157  dvlog  26158  efopn  26165  logtayl  26167  cxpcn3lem  26252  cxpcn3  26253  resqrtcn  26254  atancl  26383  atanval  26386  dvatan  26437  atancn  26438  bdaydm  27273  lltropt  27364  madess  27368  oldssmade  27369  madebdayim  27379  oldbdayim  27380  lrold  27388  topnfbey  29719  cnaddabloOLD  29829  cnidOLD  29830  cncvcOLD  29831  cnnv  29925  cnnvba  29927  cncph  30067  dfhnorm2  30370  hilablo  30408  hilid  30409  hilvc  30410  hhnv  30413  hhba  30415  hhph  30426  issh2  30457  hhssabloi  30510  hhssnv  30512  hhshsslem1  30515  imaelshi  31306  rnelshi  31307  nlelshi  31308  xrofsup  31975  ply1degltel  32661  ply1degltlss  32662  coinfliprv  33476  erdszelem2  34178  erdszelem5  34181  erdszelem8  34184  msrrcl  34529  mthmsta  34564  gg-psercn2  35173  icoreunrn  36235  icoreelrn  36237  relowlpssretop  36240  poimirlem26  36509  poimirlem27  36510  opnmbllem0  36519  dvtan  36533  fpwfvss  42153  seff  43058  sblpnf  43059  dvsconst  43079  dvsid  43080  dvsef  43081  expgrowth  43084  binomcxplemdvbinom  43102  binomcxplemdvsum  43104  binomcxplemnotnn0  43105  addcomgi  43205  dmuz  43926  dmico  44268  dvsinax  44619  fvvolioof  44695  fvvolicof  44697  dirkercncflem2  44810  fourierdlem42  44855  hoicvr  45254  ovolval3  45353