Theorem funfnd 5382

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

Syntax hints:   → wi 4  dom cdm 4748  Fun wfun 5345   Fn wfn 5346

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 5354

This theorem is referenced by:  fncofn  5861  mptsuppdifd  6454  funsssuppss  6457  suppcofn  6465  ccatalpha  11297  ennnfonelemf1  13161  dvfgg  15545  lpvtx  16066  uhgrvtxedgiedgb  16130  uhgr2edg  16193  ushgredgedg  16213  ushgredgedgloop  16215  subgruhgredgdm  16257  subuhgr  16259  subupgr  16260  subumgr  16261  subusgr  16262  vtxdfifiun  16284  trlsegvdegfi  16454  eupth2lem3lem2fi  16456  eupth2lem3lem6fi  16458  eupth2lem3lem4fi  16460  eupthvdres  16462