Theorem funfnd 5364

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 5363	. 2 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)
3	1, 2	sylib 122	1 ⊢ (𝜑 → 𝐴 Fn dom 𝐴)

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  11237  ennnfonelemf1  13100  dvfgg  15479  lpvtx  16000  uhgrvtxedgiedgb  16064  uhgr2edg  16127  ushgredgedg  16147  ushgredgedgloop  16149  subgruhgredgdm  16191  subuhgr  16193  subupgr  16194  subumgr  16195  subusgr  16196  vtxdfifiun  16218  trlsegvdegfi  16388  eupth2lem3lem2fi  16390  eupth2lem3lem6fi  16392  eupth2lem3lem4fi  16394  eupthvdres  16396