Theorem fdmi 5965

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

Syntax hints:   = wceq 1475  dom cdm 5038  ⟶wf 5800

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 196  df-an 385  df-fn 5807  df-f 5808

This theorem is referenced by:  f0cli  6278  rankvaln  8545  isnum2  8654  r0weon  8718  cfub  8954  cardcf  8957  cflecard  8958  cfle  8959  cflim2  8968  cfidm  8980  cardf  9251  smobeth  9287  inar1  9476  addcompq  9651  addcomnq  9652  mulcompq  9653  mulcomnq  9654  adderpq  9657  mulerpq  9658  addassnq  9659  mulassnq  9660  distrnq  9662  recmulnq  9665  recclnq  9667  dmrecnq  9669  lterpq  9671  ltanq  9672  ltmnq  9673  ltexnq  9676  nsmallnq  9678  ltbtwnnq  9679  prlem934  9734  ltaddpr  9735  ltexprlem2  9738  ltexprlem3  9739  ltexprlem4  9740  ltexprlem6  9742  ltexprlem7  9743  prlem936  9748  eluzel2  11568  uzssz  11583  elixx3g  12059  ndmioo  12073  elfz2  12204  fz0  12227  elfzoel1  12337  elfzoel2  12338  fzoval  12340  ltweuz  12622  fzofi  12635  dmhashres  12991  s1dm  13241  s2dm  13485  sumz  14300  sumss  14302  prod1  14513  prodss  14516  znnen  14780  unbenlem  15450  prmreclem6  15463  eldmcoa  16538  efgsdm  17966  efgsval  17967  efgsp1  17973  efgsfo  17975  efgredleme  17979  efgred  17984  gexex  18079  torsubg  18080  dmdprd  18220  dprdval  18225  iocpnfordt  20829  icomnfordt  20830  uzrest  21511  qtopbaslem  22372  retopbas  22374  tgqioo  22411  re2ndc  22412  bndth  22565  tchcph  22844  ovolficcss  23045  ismbl  23101  uniiccdif  23152  dyadmbllem  23173  opnmbllem  23175  opnmblALT  23177  mbfimaopnlem  23228  itg1addlem4  23272  dvcmul  23513  dvcmulf  23514  dvexp  23522  c1liplem1  23563  deg1n0ima  23653  pserulm  23980  psercn2  23981  psercnlem2  23982  psercnlem1  23983  psercn  23984  pserdvlem1  23985  pserdvlem2  23986  pserdv  23987  pserdv2  23988  abelth  23999  efcn  24001  efcvx  24007  eff1olem  24098  dvrelog  24183  logf1o2  24196  dvlog  24197  efopn  24204  logtayl  24206  cxpcn3lem  24288  cxpcn3  24289  resqrtcn  24290  atancl  24408  atanval  24411  dvatan  24462  atancn  24463  topnfbey  26717  cnaddabloOLD  26820  cnidOLD  26821  cncvcOLD  26822  cnnv  26916  cnnvba  26918  cncph  27058  dfhnorm2  27363  hilablo  27401  hilid  27402  hilvc  27403  hhnv  27406  hhba  27408  hhph  27419  issh2  27450  hhssabloi  27503  hhssnv  27505  hhshsslem1  27508  imaelshi  28301  rnelshi  28302  nlelshi  28303  xrofsup  28923  coinfliprv  29871  erdszelem2  30428  erdszelem5  30431  erdszelem8  30434  msrrcl  30694  mthmsta  30729  bdaydm  31077  icoreunrn  32383  icoreelrn  32385  relowlpssretop  32388  poimirlem26  32605  poimirlem27  32606  opnmbllem0  32615  dvtan  32630  seff  37530  sblpnf  37531  dvsconst  37551  dvsid  37552  dvsef  37553  expgrowth  37556  binomcxplemdvbinom  37574  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  addcomgi  37681  dvsinax  38801  fvvolioof  38882  fvvolicof  38884  dirkercncflem2  38997  fourierdlem42  39042  hoicvr  39438  ovolval3  39537