Theorem ffund 5493

Description: A mapping is a function, deduction version. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

Hypothesis

Ref	Expression
ffund.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
ffund	⊢ (𝜑 → Fun 𝐹)

Proof of Theorem ffund

Step	Hyp	Ref	Expression
1		ffund.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		ffun 5492	. 2 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)
3	1, 2	syl 14	1 ⊢ (𝜑 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 5327  ⟶wf 5329

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-fn 5336  df-f 5337

This theorem is referenced by:  swrdwrdsymbg  11294  ennnfonelemrnh  13100  ennnfonelemf1  13102  ctinfomlemom  13111  psrbaglesuppg  14751  psrelbasfun  14761  cncnp  15024  txcnp  15065  dvidlemap  15485  dvidrelem  15486  dvidsslem  15487  dvaddxx  15497  dvmulxx  15498  dvcjbr  15502  dvcj  15503  dvrecap  15507  plyaddlem1  15541  plymullem1  15542  plycoeid3  15551  uhgrfun  16001  vdegp1aid  16238  vdegp1bid  16239  wlkres  16303