Theorem fdmi 6707

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

Syntax hints:   = wceq 1563  dom cdm 5652  ⟶wf 6521

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 210  df-an 401  df-fn 6528  df-f 6529

This theorem is referenced by:  f0cli  7083  rankvaln  9759  isnum2  9919  r0weon  9984  cfub  10220  cardcf  10223  cflecard  10224  cfle  10225  cflim2  10235  cfidm  10247  cardf  10522  smobeth  10559  inar1  10748  addcompq  10923  addcomnq  10924  mulcompq  10925  mulcomnq  10926  adderpq  10929  mulerpq  10930  addassnq  10931  mulassnq  10932  distrnq  10934  recmulnq  10937  recclnq  10939  dmrecnq  10941  lterpq  10943  ltanq  10944  ltmnq  10945  ltexnq  10948  nsmallnq  10950  ltbtwnnq  10951  prlem934  11006  ltaddpr  11007  ltexprlem2  11010  ltexprlem3  11011  ltexprlem4  11012  ltexprlem6  11014  ltexprlem7  11015  prlem936  11020  eluzel2  12858  uzssz  12874  elixx3g  13376  ndmioo  13390  elfz2  13533  fz0  13558  elfzoel1  13676  elfzoel2  13677  fzoval  13679  ltweuz  13988  fzofi  14001  dmhashres  14368  s1dm  14636  s2dm  14917  sumz  15763  sumss  15765  prod1  15988  prodss  15991  znnen  16258  unbenlem  16958  prmreclem6  16971  eldmcoa  18112  efgsdm  19791  efgsval  19792  efgsp1  19798  efgsfo  19800  efgredleme  19804  efgred  19809  gexex  19914  torsubg  19915  dmdprd  20061  dprdval  20066  iocpnfordt  23333  icomnfordt  23334  uzrest  24015  qtopbaslem  24876  retopbas  24878  tgqioo  24918  re2ndc  24919  bndth  25078  tcphcph  25357  ovolficcss  25589  ismbl  25646  uniiccdif  25698  dyadmbllem  25719  opnmbllem  25721  opnmblALT  25723  mbfimaopnlem  25775  itg1addlem4  25819  dvcmul  26064  dvcmulf  26065  dvexp  26073  c1liplem1  26116  deg1n0ima  26207  pserulm  26543  psercn2  26544  psercnlem2  26545  psercnlem1  26546  psercn  26547  pserdvlem1  26548  pserdvlem2  26549  pserdv  26550  pserdv2  26551  abelth  26562  efcn  26564  efcvx  26570  eff1olem  26671  dvrelog  26760  logf1o2  26773  dvlog  26774  efopn  26781  logtayl  26783  cxpcn3lem  26870  cxpcn3  26871  resqrtcn  26872  atancl  27004  atanval  27007  dvatan  27058  atancn  27059  bdaydmOLD  27901  lltr  28013  madess  28017  oldssmade  28018  oldss  28021  madebdayim  28039  oldbdayim  28040  lrold  28048  madefi  28064  oldfi  28065  cutminmax  28087  oldfib  28528  topnfbey  30729  cnaddabloOLD  30842  cnidOLD  30843  cncvcOLD  30844  cnnv  30938  cnnvba  30940  cncph  31080  dfhnorm2  31383  hilablo  31421  hilid  31422  hilvc  31423  hhnv  31426  hhba  31428  hhph  31439  issh2  31470  hhssabloi  31523  hhssnv  31525  hhshsslem1  31528  imaelshi  32319  rnelshi  32320  nlelshi  32321  xrofsup  33024  ply1degltel  33801  ply1degleel  33802  ply1degltlss  33803  coinfliprv  34790  erdszelem2  35555  erdszelem5  35558  erdszelem8  35561  msrrcl  35906  mthmsta  35941  icoreunrn  37865  icoreelrn  37867  relowlpssretop  37870  poimirlem26  38157  poimirlem27  38158  opnmbllem0  38167  dvtan  38181  fpwfvss  44000  seff  44883  sblpnf  44884  dvsconst  44904  dvsid  44905  dvsef  44906  expgrowth  44909  binomcxplemdvbinom  44927  binomcxplemdvsum  44929  binomcxplemnotnn0  44930  addcomgi  45029  dmuz  45807  dmico  46137  dvsinax  46485  fvvolioof  46561  fvvolicof  46563  dirkercncflem2  46676  fourierdlem42  46721  hoicvr  47120  ovolval3  47219  sinnpoly  47483  fucofvalne  49954