Theorem funfnd 5383

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

Syntax hints:   → wi 4  dom cdm 4749  Fun wfun 5346   Fn wfn 5347

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 5355

This theorem is referenced by:  fncofn  5862  mptsuppdifd  6455  funsssuppss  6458  suppcofn  6466  ccatalpha  11299  ennnfonelemf1  13167  dvfgg  15551  lpvtx  16072  uhgrvtxedgiedgb  16136  uhgr2edg  16199  ushgredgedg  16219  ushgredgedgloop  16221  subgruhgredgdm  16263  subuhgr  16265  subupgr  16266  subumgr  16267  subusgr  16268  vtxdfifiun  16290  trlsegvdegfi  16460  eupth2lem3lem2fi  16462  eupth2lem3lem6fi  16464  eupth2lem3lem4fi  16466  eupthvdres  16468