Theorem funfnd 5411

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

This proof depends on syntax axioms:   → wi 4  dom cdm 4776  Fun wfun 5374   Fn wfn 5375

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 5383

This theorem is used by:  fncofn  5896  mptsuppdifd  6499  funsssuppss  6502  suppcofn  6510  ccatalpha  11403  ennnfonelemf1  13367  dvfgg  15947  lpvtx  16558  uhgrvtxedgiedgb  16622  uhgr2edg  16685  ushgredgedg  16705  ushgredgedgloop  16707  subgruhgredgdm  16749  subuhgr  16751  subupgr  16752  subumgr  16753  subusgr  16754  vtxdfifiun  16776  trlsegvdegfi  16946  eupth2lem3lem2fi  16948  eupth2lem3lem6fi  16950  eupth2lem3lem4fi  16952  eupthvdres  16954