Theorem funfnd 6556

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 6555	. 2 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)
3	1, 2	sylib 221	1 ⊢ (𝜑 → 𝐴 Fn dom 𝐴)

Syntax hints:   → wi 4  dom cdm 5652  Fun wfun 6519   Fn wfn 6520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-fn 6528

This theorem is referenced by:  fncofn  6642  resfunexg  7203  ralima  7225  funiunfv  7236  funelss  8032  funsssuppss  8174  frrlem4  8274  smores2  8329  tfrlem1  8350  resfnfinfin  9282  resfifsupp  9345  ordtypelem4  9471  ordtypelem9  9476  ordtypelem10  9477  brdom3  10500  brdom5  10501  brdom4  10502  fpwwe2lem10  10613  hashimarn  14467  resunimafz0  14472  isstruct2  17199  invf  17815  lindfrn  21931  psdmul  22289  ofco2  22569  dfac14  23736  perfdvf  26023  c1lip2  26118  taylf  26482  elno2  27776  noinfbnd2lem1  27852  noetainflem4  27862  lpvtx  29327  upgrle2  29364  uhgrvtxedgiedgb  29395  uhgr2edg  29467  ushgredgedg  29488  ushgredgedgloop  29490  subgruhgredgd  29543  subuhgr  29545  subupgr  29546  subumgr  29547  subusgr  29548  upgrres  29565  umgrres  29566  vtxdun  29740  upgrewlkle2  29865  eupthvdres  30495  cycpmfvlem  33345  cycpmfv3  33348  sitgf  34654  cardpred  35398  nummin  35399  bj-gabima  37437  gneispace  44722  gneispacef2  44724  funimaeq  45819  limsupresxr  46338  liminfresxr  46339  funcoressn  47634  isubgr0uhgr  48493  upgrimwlklem1  48517