Theorem funfnd 5357

Description: A function is a function over its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypothesis

Ref	Expression
funfnd.1	|- ( ph -> Fun A )

Assertion

Ref	Expression
funfnd	|- ( ph -> A Fn dom A )

Proof of Theorem funfnd

Step	Hyp	Ref	Expression
1		funfnd.1	. 2 |- ( ph -> Fun A )
2		funfn 5356	. 2 |- ( Fun A <-> A Fn dom A )
3	1, 2	sylib 122	1 |- ( ph -> A Fn dom A )

Syntax hints:   -> wi 4   dom cdm 4725   Fun wfun 5320   Fn wfn 5321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1497  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-fn 5329

This theorem is referenced by:  fncofn  5832  ccatalpha  11194  ennnfonelemf1  13057  dvfgg  15431  lpvtx  15949  uhgrvtxedgiedgb  16013  uhgr2edg  16076  ushgredgedg  16096  ushgredgedgloop  16098  subgruhgredgdm  16140  subuhgr  16142  subupgr  16143  subumgr  16144  subusgr  16145  vtxdfifiun  16167  trlsegvdegfi  16337  eupth2lem3lem2fi  16339  eupth2lem3lem6fi  16341  eupth2lem3lem4fi  16343  eupthvdres  16345