Theorem funfnd 5403

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

Syntax hints:   -> wi 4   dom cdm 4769   Fun wfun 5366   Fn wfn 5367

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 1502  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-fn 5375

This theorem is referenced by:  fncofn  5884  mptsuppdifd  6485  funsssuppss  6488  suppcofn  6496  ccatalpha  11359  ennnfonelemf1  13287  dvfgg  15712  lpvtx  16234  uhgrvtxedgiedgb  16298  uhgr2edg  16361  ushgredgedg  16381  ushgredgedgloop  16383  subgruhgredgdm  16425  subuhgr  16427  subupgr  16428  subumgr  16429  subusgr  16430  vtxdfifiun  16452  trlsegvdegfi  16622  eupth2lem3lem2fi  16624  eupth2lem3lem6fi  16626  eupth2lem3lem4fi  16628  eupthvdres  16630