Theorem funfnd 5383

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

Syntax hints:   -> wi 4   dom cdm 4749   Fun wfun 5346   Fn wfn 5347

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 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-fn 5355

This theorem is referenced by:  fncofn  5862  mptsuppdifd  6455  funsssuppss  6458  suppcofn  6466  ccatalpha  11301  ennnfonelemf1  13169  dvfgg  15553  lpvtx  16074  uhgrvtxedgiedgb  16138  uhgr2edg  16201  ushgredgedg  16221  ushgredgedgloop  16223  subgruhgredgdm  16265  subuhgr  16267  subupgr  16268  subumgr  16269  subusgr  16270  vtxdfifiun  16292  trlsegvdegfi  16462  eupth2lem3lem2fi  16464  eupth2lem3lem6fi  16466  eupth2lem3lem4fi  16468  eupthvdres  16470