Theorem funfnd 5408

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

This proof depends on syntax axioms:   → wi 4  dom cdm 4774  Fun wfun 5371   Fn wfn 5372

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231  df-fn 5380

This theorem is used by:  fncofn  5893  mptsuppdifd  6495  funsssuppss  6498  suppcofn  6506  ccatalpha  11383  ennnfonelemf1  13311  dvfgg  15791  lpvtx  16332  uhgrvtxedgiedgb  16396  uhgr2edg  16459  ushgredgedg  16479  ushgredgedgloop  16481  subgruhgredgdm  16523  subuhgr  16525  subupgr  16526  subumgr  16527  subusgr  16528  vtxdfifiun  16550  trlsegvdegfi  16720  eupth2lem3lem2fi  16722  eupth2lem3lem6fi  16724  eupth2lem3lem4fi  16726  eupthvdres  16728