Theorem ffnd 5231

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

Hypothesis

Ref	Expression
ffnd.1	|- ( ph -> F : A --> B )

Assertion

Ref	Expression
ffnd	|- ( ph -> F Fn A )

Proof of Theorem ffnd

Step	Hyp	Ref	Expression
1		ffnd.1	. 2 |- ( ph -> F : A --> B )
2		ffn 5230	. 2 |- ( F : A --> B -> F Fn A )
3	1, 2	syl 14	1 |- ( ph -> F Fn A )

Syntax hints:   -> wi 4   Fn wfn 5076   -->wf 5077

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

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

This theorem is referenced by:  offeq  5949  difinfsn  6937  ctssdc  6950  seqvalcd  10125  seq3feq2  10136  seq3feq  10138  seqfeq3  10178  ser0f  10181  facnn  10366  fac0  10367  resunimafz0  10467  seq3shft  10503  fisumss  11053  efcvgfsum  11224  ennnfonelemfun  11775  ennnfonelemf1  11776  cnrest2  12247  lmss  12257  lmtopcnp  12261  upxp  12283  uptx  12285  cnmpt11  12294  cnmpt21  12302  cnmpt22f  12306  cnmptcom  12309  psmetxrge0  12321  isxmet2d  12337  blelrnps  12408  blelrn  12409  xmetresbl  12429  comet  12488  bdxmet  12490  xmettx  12499  dvidlemap  12615  dvaddxxbr  12620  dvmulxxbr  12621  nninfalllemn  12894  nninfall  12896  nninfsellemeqinf  12904  nninffeq  12908  refeq  12915