Theorem ffnd 5273

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 5272	. 2 |- ( F : A --> B -> F Fn A )
3	1, 2	syl 14	1 |- ( ph -> F Fn A )

Syntax hints:   -> wi 4   Fn wfn 5118   -->wf 5119

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 5127

This theorem is referenced by:  offeq  5995  difinfsn  6985  ctssdc  6998  seqvalcd  10235  seq3feq2  10246  seq3feq  10248  seqfeq3  10288  ser0f  10291  facnn  10476  fac0  10477  resunimafz0  10577  seq3shft  10613  fisumss  11164  prodf1f  11315  efcvgfsum  11376  ennnfonelemfun  11933  ennnfonelemf1  11934  cnrest2  12408  lmss  12418  lmtopcnp  12422  upxp  12444  uptx  12446  cnmpt11  12455  cnmpt21  12463  cnmpt22f  12467  cnmptcom  12470  hmeof1o2  12480  psmetxrge0  12504  isxmet2d  12520  blelrnps  12591  blelrn  12592  xmetresbl  12612  comet  12671  bdxmet  12673  xmettx  12682  dvidlemap  12832  dvaddxxbr  12837  dvmulxxbr  12838  dvrecap  12849  nninfalllemn  13205  nninfall  13207  nninfsellemeqinf  13215  nninffeq  13219  refeq  13226