Theorem funfnd 6512

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

Syntax hints:   → wi 4  dom cdm 5616  Fun wfun 6475   Fn wfn 6476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-fn 6484

This theorem is referenced by:  fncofn  6598  resfunexg  7149  ralima  7171  funiunfv  7182  funelss  7979  funsssuppss  8120  frrlem4  8219  smores2  8274  tfrlem1  8295  resfnfinfin  9221  resfifsupp  9281  ordtypelem4  9407  ordtypelem9  9412  ordtypelem10  9413  brdom3  10416  brdom5  10417  brdom4  10418  fpwwe2lem10  10528  hashimarn  14344  resunimafz0  14349  isstruct2  17057  invf  17672  lindfrn  21756  psdmul  22079  ofco2  22364  dfac14  23531  perfdvf  25829  c1lip2  25928  taylf  26293  elno2  27591  noinfbnd2lem1  27667  noetainflem4  27677  lpvtx  29044  upgrle2  29081  uhgrvtxedgiedgb  29112  uhgr2edg  29184  ushgredgedg  29205  ushgredgedgloop  29207  subgruhgredgd  29260  subuhgr  29262  subupgr  29263  subumgr  29264  subusgr  29265  upgrres  29282  umgrres  29283  vtxdun  29458  upgrewlkle2  29583  eupthvdres  30210  cycpmfvlem  33076  cycpmfv3  33079  sitgf  34355  cardpred  35098  nummin  35099  bj-gabima  36973  gneispace  44166  gneispacef2  44168  funimaeq  45282  limsupresxr  45803  liminfresxr  45804  funcoressn  47072  isubgr0uhgr  47903  upgrimwlklem1  47927