Theorem funfnd 5388

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 5387	. 2 |- ( Fun A <-> A Fn dom A )
3	1, 2	sylib 122	1 |- ( ph -> A Fn dom A )

Syntax hints:   -> wi 4   dom cdm 4754   Fun wfun 5351   Fn wfn 5352

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 1498  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-fn 5360

This theorem is referenced by:  fncofn  5867  mptsuppdifd  6468  funsssuppss  6471  suppcofn  6479  ccatalpha  11326  ennnfonelemf1  13253  dvfgg  15679  lpvtx  16200  uhgrvtxedgiedgb  16264  uhgr2edg  16327  ushgredgedg  16347  ushgredgedgloop  16349  subgruhgredgdm  16391  subuhgr  16393  subupgr  16394  subumgr  16395  subusgr  16396  vtxdfifiun  16418  trlsegvdegfi  16588  eupth2lem3lem2fi  16590  eupth2lem3lem6fi  16592  eupth2lem3lem4fi  16594  eupthvdres  16596