Theorem ffnd 5361

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

Syntax hints:   -> wi 4   Fn wfn 5206   -->wf 5207

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-f 5215

This theorem is referenced by:  offeq  6089  difinfsn  7092  ctssdc  7105  nnnninfeq  7119  nninfdcinf  7162  nninfwlporlemd  7163  nninfwlporlem  7164  seqvalcd  10432  seq3feq2  10443  seq3feq  10445  seqfeq3  10485  ser0f  10488  facnn  10678  fac0  10679  resunimafz0  10782  seq3shft  10818  fisumss  11371  prodf1f  11522  efcvgfsum  11646  ennnfonelemfun  12388  ennnfonelemf1  12389  mhmf1o  12738  mhmima  12752  mhmeql  12753  grpinvf1o  12816  cnrest2  13369  lmss  13379  lmtopcnp  13383  upxp  13405  uptx  13407  cnmpt11  13416  cnmpt21  13424  cnmpt22f  13428  cnmptcom  13431  hmeof1o2  13441  psmetxrge0  13465  isxmet2d  13481  blelrnps  13552  blelrn  13553  xmetresbl  13573  comet  13632  bdxmet  13634  xmettx  13643  dvidlemap  13793  dvaddxxbr  13798  dvmulxxbr  13799  dvrecap  13810  nninfall  14381  nninfsellemeqinf  14388  nninffeq  14392  refeq  14399