Theorem funfnd 5364

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

Syntax hints:   -> wi 4   dom cdm 4731   Fun wfun 5327   Fn wfn 5328

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 2213

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

This theorem is referenced by:  fncofn  5840  mptsuppdifd  6433  funsssuppss  6436  suppcofn  6444  ccatalpha  11256  ennnfonelemf1  13119  dvfgg  15499  lpvtx  16020  uhgrvtxedgiedgb  16084  uhgr2edg  16147  ushgredgedg  16167  ushgredgedgloop  16169  subgruhgredgdm  16211  subuhgr  16213  subupgr  16214  subumgr  16215  subusgr  16216  vtxdfifiun  16238  trlsegvdegfi  16408  eupth2lem3lem2fi  16410  eupth2lem3lem6fi  16412  eupth2lem3lem4fi  16414  eupthvdres  16416