Theorem fdmi 6019

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

Syntax hints:   = wceq 1480  dom cdm 5084  ⟶wf 5853

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 197  df-an 386  df-fn 5860  df-f 5861

This theorem is referenced by:  f0cli  6336  rankvaln  8622  isnum2  8731  r0weon  8795  cfub  9031  cardcf  9034  cflecard  9035  cfle  9036  cflim2  9045  cfidm  9057  cardf  9332  smobeth  9368  inar1  9557  addcompq  9732  addcomnq  9733  mulcompq  9734  mulcomnq  9735  adderpq  9738  mulerpq  9739  addassnq  9740  mulassnq  9741  distrnq  9743  recmulnq  9746  recclnq  9748  dmrecnq  9750  lterpq  9752  ltanq  9753  ltmnq  9754  ltexnq  9757  nsmallnq  9759  ltbtwnnq  9760  prlem934  9815  ltaddpr  9816  ltexprlem2  9819  ltexprlem3  9820  ltexprlem4  9821  ltexprlem6  9823  ltexprlem7  9824  prlem936  9829  eluzel2  11652  uzssz  11667  elixx3g  12146  ndmioo  12160  elfz2  12291  fz0  12314  elfzoel1  12425  elfzoel2  12426  fzoval  12428  ltweuz  12716  fzofi  12729  dmhashres  13085  s1dm  13343  s2dm  13587  sumz  14402  sumss  14404  prod1  14618  prodss  14621  znnen  14885  unbenlem  15555  prmreclem6  15568  eldmcoa  16655  efgsdm  18083  efgsval  18084  efgsp1  18090  efgsfo  18092  efgredleme  18096  efgred  18101  gexex  18196  torsubg  18197  dmdprd  18337  dprdval  18342  iocpnfordt  20959  icomnfordt  20960  uzrest  21641  qtopbaslem  22502  retopbas  22504  tgqioo  22543  re2ndc  22544  bndth  22697  tchcph  22976  ovolficcss  23178  ismbl  23234  uniiccdif  23286  dyadmbllem  23307  opnmbllem  23309  opnmblALT  23311  mbfimaopnlem  23362  itg1addlem4  23406  dvcmul  23647  dvcmulf  23648  dvexp  23656  c1liplem1  23697  deg1n0ima  23787  pserulm  24114  psercn2  24115  psercnlem2  24116  psercnlem1  24117  psercn  24118  pserdvlem1  24119  pserdvlem2  24120  pserdv  24121  pserdv2  24122  abelth  24133  efcn  24135  efcvx  24141  eff1olem  24232  dvrelog  24317  logf1o2  24330  dvlog  24331  efopn  24338  logtayl  24340  cxpcn3lem  24422  cxpcn3  24423  resqrtcn  24424  atancl  24542  atanval  24545  dvatan  24596  atancn  24597  topnfbey  27213  cnaddabloOLD  27324  cnidOLD  27325  cncvcOLD  27326  cnnv  27420  cnnvba  27422  cncph  27562  dfhnorm2  27867  hilablo  27905  hilid  27906  hilvc  27907  hhnv  27910  hhba  27912  hhph  27923  issh2  27954  hhssabloi  28007  hhssnv  28009  hhshsslem1  28012  imaelshi  28805  rnelshi  28806  nlelshi  28807  xrofsup  29418  coinfliprv  30367  erdszelem2  30935  erdszelem5  30938  erdszelem8  30941  msrrcl  31201  mthmsta  31236  bdaydm  31594  icoreunrn  32878  icoreelrn  32880  relowlpssretop  32883  poimirlem26  33106  poimirlem27  33107  opnmbllem0  33116  dvtan  33131  seff  38029  sblpnf  38030  dvsconst  38050  dvsid  38051  dvsef  38052  expgrowth  38055  binomcxplemdvbinom  38073  binomcxplemdvsum  38075  binomcxplemnotnn0  38076  addcomgi  38181  dmuz  38950  dvsinax  39463  fvvolioof  39543  fvvolicof  39545  dirkercncflem2  39658  fourierdlem42  39703  hoicvr  40099  ovolval3  40198