Theorem funfnd 5406

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

Syntax hints:   → wi 4  dom cdm 4772  Fun wfun 5369   Fn wfn 5370

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 1502  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-fn 5378

This theorem is referenced by:  fncofn  5887  mptsuppdifd  6489  funsssuppss  6492  suppcofn  6500  ccatalpha  11364  ennnfonelemf1  13292  dvfgg  15772  lpvtx  16303  uhgrvtxedgiedgb  16367  uhgr2edg  16430  ushgredgedg  16450  ushgredgedgloop  16452  subgruhgredgdm  16494  subuhgr  16496  subupgr  16497  subumgr  16498  subusgr  16499  vtxdfifiun  16521  trlsegvdegfi  16691  eupth2lem3lem2fi  16693  eupth2lem3lem6fi  16695  eupth2lem3lem4fi  16697  eupthvdres  16699