Theorem funfnd 6529

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

Syntax hints:   → wi 4  dom cdm 5631  Fun wfun 6492   Fn wfn 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-fn 6501

This theorem is referenced by:  fncofn  6615  resfunexg  7170  ralima  7192  funiunfv  7203  funelss  8000  funsssuppss  8140  frrlem4  8239  smores2  8294  tfrlem1  8315  resfnfinfin  9247  resfifsupp  9310  ordtypelem4  9436  ordtypelem9  9441  ordtypelem10  9442  brdom3  10450  brdom5  10451  brdom4  10452  fpwwe2lem10  10563  hashimarn  14402  resunimafz0  14407  isstruct2  17119  invf  17735  lindfrn  21801  psdmul  22132  ofco2  22416  dfac14  23583  perfdvf  25870  c1lip2  25965  taylf  26326  elno2  27618  noinfbnd2lem1  27694  noetainflem4  27704  lpvtx  29137  upgrle2  29174  uhgrvtxedgiedgb  29205  uhgr2edg  29277  ushgredgedg  29298  ushgredgedgloop  29300  subgruhgredgd  29353  subuhgr  29355  subupgr  29356  subumgr  29357  subusgr  29358  upgrres  29375  umgrres  29376  vtxdun  29550  upgrewlkle2  29675  eupthvdres  30305  cycpmfvlem  33173  cycpmfv3  33176  sitgf  34491  cardpred  35235  nummin  35236  bj-gabima  37247  gneispace  44561  gneispacef2  44563  funimaeq  45675  limsupresxr  46194  liminfresxr  46195  funcoressn  47490  isubgr0uhgr  48349  upgrimwlklem1  48373