Theorem funfnd 6569

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

Syntax hints:   → wi 4  dom cdm 5663  Fun wfun 6532   Fn wfn 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-fn 6541

This theorem is referenced by:  fncofn  6654  resfunexg  7215  ralima  7237  funiunfv  7248  funelss  8045  funsssuppss  8187  frrlem4  8287  smores2  8342  tfrlem1  8363  resfnfinfin  9295  resfifsupp  9358  ordtypelem4  9484  ordtypelem9  9489  ordtypelem10  9490  brdom3  10513  brdom5  10514  brdom4  10515  fpwwe2lem10  10626  hashimarn  14479  resunimafz0  14484  isstruct2  17210  invf  17826  lindfrn  21952  psdmul  22310  ofco2  22589  dfac14  23756  perfdvf  26043  c1lip2  26138  taylf  26502  elno2  27796  noinfbnd2lem1  27872  noetainflem4  27882  lpvtx  29396  upgrle2  29433  uhgrvtxedgiedgb  29464  uhgr2edg  29536  ushgredgedg  29557  ushgredgedgloop  29559  subgruhgredgd  29612  subuhgr  29614  subupgr  29615  subumgr  29616  subusgr  29617  upgrres  29634  umgrres  29635  vtxdun  29809  upgrewlkle2  29934  eupthvdres  30564  cycpmfvlem  33410  cycpmfv3  33413  sitgf  34715  cardpred  35461  nummin  35462  bj-gabima  37554  gneispace  44840  gneispacef2  44842  funimaeq  45941  limsupresxr  46460  liminfresxr  46461  funcoressn  47756  isubgr0uhgr  48615  upgrimwlklem1  48639