Theorem ffnd 5338

Description: A mapping is a function with domain, deduction form. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypothesis

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

Assertion

Ref	Expression
ffnd	⊢ (𝜑 → 𝐹 Fn 𝐴)

Proof of Theorem ffnd

Step	Hyp	Ref	Expression
1		ffnd.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		ffn 5337	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 5183  ⟶wf 5184

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

This theorem depends on definitions:  df-bi 116  df-f 5192

This theorem is referenced by:  offeq  6063  difinfsn  7065  ctssdc  7078  nnnninfeq  7092  seqvalcd  10394  seq3feq2  10405  seq3feq  10407  seqfeq3  10447  ser0f  10450  facnn  10640  fac0  10641  resunimafz0  10744  seq3shft  10780  fisumss  11333  prodf1f  11484  efcvgfsum  11608  ennnfonelemfun  12350  ennnfonelemf1  12351  cnrest2  12876  lmss  12886  lmtopcnp  12890  upxp  12912  uptx  12914  cnmpt11  12923  cnmpt21  12931  cnmpt22f  12935  cnmptcom  12938  hmeof1o2  12948  psmetxrge0  12972  isxmet2d  12988  blelrnps  13059  blelrn  13060  xmetresbl  13080  comet  13139  bdxmet  13141  xmettx  13150  dvidlemap  13300  dvaddxxbr  13305  dvmulxxbr  13306  dvrecap  13317  nninfall  13889  nninfsellemeqinf  13896  nninffeq  13900  refeq  13907