Theorem funfnd 5388

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

Hypothesis

Ref	Expression
funfnd.1	⊢ (𝜑 → Fun 𝐴)

Assertion

Ref	Expression
funfnd	⊢ (𝜑 → 𝐴 Fn dom 𝐴)

Proof of Theorem funfnd

Step	Hyp	Ref	Expression
1		funfnd.1	. 2 ⊢ (𝜑 → Fun 𝐴)
2		funfn 5387	. 2 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)
3	1, 2	sylib 122	1 ⊢ (𝜑 → 𝐴 Fn dom 𝐴)

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  15665  lpvtx  16186  uhgrvtxedgiedgb  16250  uhgr2edg  16313  ushgredgedg  16333  ushgredgedgloop  16335  subgruhgredgdm  16377  subuhgr  16379  subupgr  16380  subumgr  16381  subusgr  16382  vtxdfifiun  16404  trlsegvdegfi  16574  eupth2lem3lem2fi  16576  eupth2lem3lem6fi  16578  eupth2lem3lem4fi  16580  eupthvdres  16582