Theorem funfnd 6599

Description: A function is a function on its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypothesis

Ref	Expression
funfnd.1	⊢ (𝜑 → Fun 𝐴)

Assertion

Ref	Expression
funfnd	⊢ (𝜑 → 𝐴 Fn dom 𝐴)

Proof of Theorem funfnd

Step	Hyp	Ref	Expression
1		funfnd.1	. 2 ⊢ (𝜑 → Fun 𝐴)
2		funfn 6598	. 2 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)
3	1, 2	sylib 218	1 ⊢ (𝜑 → 𝐴 Fn dom 𝐴)

Syntax hints:   → wi 4  dom cdm 5689  Fun wfun 6557   Fn wfn 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-fn 6566

This theorem is referenced by:  fncofn  6686  resfunexg  7235  ralima  7257  funiunfv  7268  funelss  8071  funsssuppss  8214  frrlem4  8313  wfrlem4OLD  8351  smores2  8393  tfrlem1  8415  resfnfinfin  9375  resfifsupp  9435  ordtypelem4  9559  ordtypelem9  9564  ordtypelem10  9565  brdom3  10566  brdom5  10567  brdom4  10568  fpwwe2lem10  10678  hashimarn  14476  resunimafz0  14481  isstruct2  17183  invf  17816  lindfrn  21859  psdmul  22188  ofco2  22473  dfac14  23642  perfdvf  25953  c1lip2  26052  taylf  26417  elno2  27714  noinfbnd2lem1  27790  noetainflem4  27800  lpvtx  29100  upgrle2  29137  uhgrvtxedgiedgb  29168  uhgr2edg  29240  ushgredgedg  29261  ushgredgedgloop  29263  subgruhgredgd  29316  subuhgr  29318  subupgr  29319  subumgr  29320  subusgr  29321  upgrres  29338  umgrres  29339  vtxdun  29514  upgrewlkle2  29639  eupthvdres  30264  cycpmfvlem  33115  cycpmfv3  33118  sitgf  34329  cardpred  35083  nummin  35084  bj-gabima  36923  gneispace  44124  gneispacef2  44126  funimaeq  45191  limsupresxr  45722  liminfresxr  45723  funcoressn  46992  isubgr0uhgr  47797