Theorem fdmi 6680

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

Syntax hints:   = wceq 1542  dom cdm 5631  ⟶wf 6495

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 207  df-an 396  df-fn 6502  df-f 6503

This theorem is referenced by:  f0cli  7051  rankvaln  9723  isnum2  9869  r0weon  9934  cfub  10171  cardcf  10174  cflecard  10175  cfle  10176  cflim2  10185  cfidm  10197  cardf  10472  smobeth  10509  inar1  10698  addcompq  10873  addcomnq  10874  mulcompq  10875  mulcomnq  10876  adderpq  10879  mulerpq  10880  addassnq  10881  mulassnq  10882  distrnq  10884  recmulnq  10887  recclnq  10889  dmrecnq  10891  lterpq  10893  ltanq  10894  ltmnq  10895  ltexnq  10898  nsmallnq  10900  ltbtwnnq  10901  prlem934  10956  ltaddpr  10957  ltexprlem2  10960  ltexprlem3  10961  ltexprlem4  10962  ltexprlem6  10964  ltexprlem7  10965  prlem936  10970  eluzel2  12793  uzssz  12809  elixx3g  13311  ndmioo  13325  elfz2  13468  fz0  13493  elfzoel1  13611  elfzoel2  13612  fzoval  13614  ltweuz  13923  fzofi  13936  dmhashres  14303  s1dm  14571  s2dm  14852  sumz  15684  sumss  15686  prod1  15909  prodss  15912  znnen  16179  unbenlem  16879  prmreclem6  16892  eldmcoa  18032  efgsdm  19705  efgsval  19706  efgsp1  19712  efgsfo  19714  efgredleme  19718  efgred  19723  gexex  19828  torsubg  19829  dmdprd  19975  dprdval  19980  iocpnfordt  23180  icomnfordt  23181  uzrest  23862  qtopbaslem  24723  retopbas  24725  tgqioo  24765  re2ndc  24766  bndth  24925  tcphcph  25204  ovolficcss  25436  ismbl  25493  uniiccdif  25545  dyadmbllem  25566  opnmbllem  25568  opnmblALT  25570  mbfimaopnlem  25622  itg1addlem4  25666  dvcmul  25911  dvcmulf  25912  dvexp  25920  c1liplem1  25963  deg1n0ima  26054  pserulm  26387  psercn2  26388  psercnlem2  26389  psercnlem1  26390  psercn  26391  pserdvlem1  26392  pserdvlem2  26393  pserdv  26394  pserdv2  26395  abelth  26406  efcn  26408  efcvx  26414  eff1olem  26512  dvrelog  26601  logf1o2  26614  dvlog  26615  efopn  26622  logtayl  26624  cxpcn3lem  26711  cxpcn3  26712  resqrtcn  26713  atancl  26845  atanval  26848  dvatan  26899  atancn  26900  bdaydm  27742  lltr  27854  madess  27858  oldssmade  27859  oldss  27862  madebdayim  27880  oldbdayim  27881  lrold  27889  madefi  27905  oldfi  27906  cutminmax  27928  oldfib  28369  topnfbey  30539  cnaddabloOLD  30652  cnidOLD  30653  cncvcOLD  30654  cnnv  30748  cnnvba  30750  cncph  30890  dfhnorm2  31193  hilablo  31231  hilid  31232  hilvc  31233  hhnv  31236  hhba  31238  hhph  31249  issh2  31280  hhssabloi  31333  hhssnv  31335  hhshsslem1  31338  imaelshi  32129  rnelshi  32130  nlelshi  32131  xrofsup  32840  ply1degltel  33654  ply1degleel  33655  ply1degltlss  33656  coinfliprv  34627  erdszelem2  35374  erdszelem5  35377  erdszelem8  35380  msrrcl  35725  mthmsta  35760  icoreunrn  37675  icoreelrn  37677  relowlpssretop  37680  poimirlem26  37967  poimirlem27  37968  opnmbllem0  37977  dvtan  37991  fpwfvss  43839  seff  44736  sblpnf  44737  dvsconst  44757  dvsid  44758  dvsef  44759  expgrowth  44762  binomcxplemdvbinom  44780  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  addcomgi  44882  dmuz  45663  dmico  45993  dvsinax  46341  fvvolioof  46417  fvvolicof  46419  dirkercncflem2  46532  fourierdlem42  46577  hoicvr  46976  ovolval3  47075  sinnpoly  47333  fucofvalne  49794