Theorem funfnd 6465

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

Syntax hints:   → wi 4  dom cdm 5589  Fun wfun 6427   Fn wfn 6428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-fn 6436

This theorem is referenced by:  fncofn  6548  resfunexg  7091  funiunfv  7121  funelss  7888  funsssuppss  8006  frrlem4  8105  wfrlem4OLD  8143  smores2  8185  tfrlem1  8207  resfnfinfin  9099  resfifsupp  9156  ordtypelem4  9280  ordtypelem9  9285  ordtypelem10  9286  brdom3  10284  brdom5  10285  brdom4  10286  fpwwe2lem10  10396  hashimarn  14155  resunimafz0  14157  isstruct2  16850  invf  17480  lindfrn  21028  ofco2  21600  dfac14  22769  perfdvf  25067  c1lip2  25162  taylf  25520  lpvtx  27438  upgrle2  27475  uhgrvtxedgiedgb  27506  uhgr2edg  27575  ushgredgedg  27596  ushgredgedgloop  27598  subgruhgredgd  27651  subuhgr  27653  subupgr  27654  subumgr  27655  subusgr  27656  upgrres  27673  umgrres  27674  vtxdun  27848  upgrewlkle2  27973  eupthvdres  28599  cycpmfvlem  31379  cycpmfv3  31382  sitgf  32314  cardpred  33062  nummin  33063  elno2  33857  noinfbnd2lem1  33933  noetainflem4  33943  bj-gabima  35128  gneispace  41744  gneispacef2  41746  funimaeq  42792  limsupresxr  43307  liminfresxr  43308  funcoressn  44536