Theorem fdmi 6303

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

Syntax hints:   = wceq 1601  dom cdm 5357  ⟶wf 6133

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 199  df-an 387  df-fn 6140  df-f 6141

This theorem is referenced by:  f0cli  6636  rankvaln  8961  isnum2  9106  r0weon  9170  cfub  9408  cardcf  9411  cflecard  9412  cfle  9413  cflim2  9422  cfidm  9434  cardf  9709  smobeth  9745  inar1  9934  addcompq  10109  addcomnq  10110  mulcompq  10111  mulcomnq  10112  adderpq  10115  mulerpq  10116  addassnq  10117  mulassnq  10118  distrnq  10120  recmulnq  10123  recclnq  10125  dmrecnq  10127  lterpq  10129  ltanq  10130  ltmnq  10131  ltexnq  10134  nsmallnq  10136  ltbtwnnq  10137  prlem934  10192  ltaddpr  10193  ltexprlem2  10196  ltexprlem3  10197  ltexprlem4  10198  ltexprlem6  10200  ltexprlem7  10201  prlem936  10206  eluzel2  12001  uzssz  12016  elixx3g  12504  ndmioo  12518  elfz2  12654  fz0  12677  elfzoel1  12791  elfzoel2  12792  fzoval  12794  ltweuz  13083  fzofi  13096  dmhashres  13450  s1dm  13702  s2dm  14045  sumz  14864  sumss  14866  prod1  15081  prodss  15084  znnen  15349  unbenlem  16020  prmreclem6  16033  eldmcoa  17104  efgsdm  18531  efgsval  18532  efgsp1  18538  efgsfo  18541  efgredleme  18545  efgred  18551  gexex  18646  torsubg  18647  dmdprd  18788  dprdval  18793  iocpnfordt  21431  icomnfordt  21432  uzrest  22113  qtopbaslem  22974  retopbas  22976  tgqioo  23015  re2ndc  23016  bndth  23169  tcphcph  23447  ovolficcss  23677  ismbl  23734  uniiccdif  23786  dyadmbllem  23807  opnmbllem  23809  opnmblALT  23811  mbfimaopnlem  23863  itg1addlem4  23907  dvcmul  24148  dvcmulf  24149  dvexp  24157  c1liplem1  24200  deg1n0ima  24290  pserulm  24617  psercn2  24618  psercnlem2  24619  psercnlem1  24620  psercn  24621  pserdvlem1  24622  pserdvlem2  24623  pserdv  24624  pserdv2  24625  abelth  24636  efcn  24638  efcvx  24644  eff1olem  24736  dvrelog  24824  logf1o2  24837  dvlog  24838  efopn  24845  logtayl  24847  cxpcn3lem  24932  cxpcn3  24933  resqrtcn  24934  atancl  25063  atanval  25066  dvatan  25117  atancn  25118  topnfbey  27904  cnaddabloOLD  28012  cnidOLD  28013  cncvcOLD  28014  cnnv  28108  cnnvba  28110  cncph  28250  dfhnorm2  28555  hilablo  28593  hilid  28594  hilvc  28595  hhnv  28598  hhba  28600  hhph  28611  issh2  28642  hhssabloi  28695  hhssnv  28697  hhshsslem1  28700  imaelshi  29493  rnelshi  29494  nlelshi  29495  xrofsup  30102  coinfliprv  31147  erdszelem2  31777  erdszelem5  31780  erdszelem8  31783  msrrcl  32043  mthmsta  32078  bdaydm  32483  icoreunrn  33805  icoreelrn  33807  relowlpssretop  33810  poimirlem26  34066  poimirlem27  34067  opnmbllem0  34076  dvtan  34090  seff  39474  sblpnf  39475  dvsconst  39495  dvsid  39496  dvsef  39497  expgrowth  39500  binomcxplemdvbinom  39518  binomcxplemdvsum  39520  binomcxplemnotnn0  39521  addcomgi  39624  dmuz  40367  dmico  40710  dvsinax  41065  fvvolioof  41143  fvvolicof  41145  dirkercncflem2  41258  fourierdlem42  41303  hoicvr  41699  ovolval3  41798