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  11329  ennnfonelemf1  13257  dvfgg  15683  lpvtx  16204  uhgrvtxedgiedgb  16268  uhgr2edg  16331  ushgredgedg  16351  ushgredgedgloop  16353  subgruhgredgdm  16395  subuhgr  16397  subupgr  16398  subumgr  16399  subusgr  16400  vtxdfifiun  16422  trlsegvdegfi  16592  eupth2lem3lem2fi  16594  eupth2lem3lem6fi  16596  eupth2lem3lem4fi  16598  eupthvdres  16600