Theorem ffnd 5529

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

Syntax hints:   -> wi 4   Fn wfn 5367   -->wf 5368

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 5376

This theorem is referenced by:  offeq  6306  caofid0l  6319  caofid0r  6320  caofid1  6321  caofid2  6322  fvdifsuppst  6474  suppsnopdc  6480  suppssdc  6490  suppssrst  6491  suppssrgst  6492  suppofss1dcl  6494  suppofss2dcl  6495  mapen  7136  difinfsn  7430  ctssdc  7443  nnnninfeq  7458  nninfdcinf  7501  nninfwlporlemd  7502  nninfwlporlem  7503  ofnegsub  9282  seqvalcd  10876  seq3feq2  10891  seq3feq  10895  seqf1oglem2  10935  seqfeq3  10944  ser0f  10949  facnn  11143  fac0  11144  resunimafz0  11252  wrdfn  11297  swrdvalfn  11406  pfxfn  11433  pfxid  11436  cats1un  11471  seq3shft  11581  fisumss  12137  prodf1f  12288  efcvgfsum  12412  nninfctlemfo  12795  ennnfonelemfun  13286  ennnfonelemf1  13287  mhmf1o  13754  resmhm2b  13773  mhmima  13775  mhmeql  13776  gzsumwmhm  13780  grpinvf1o  13852  ghmrn  14037  ghmpreima  14046  ghmeql  14047  ghmnsgima  14048  ghmnsgpreima  14049  ghmeqker  14051  ghmf1o  14055  gsumclfi  14136  gsumf1ofi  14137  gsumsubmclfi  14140  prdsplusgsgrpcl  14167  prdssgrpd  14168  prdsplusgcl  14169  prdsidlem  14170  prdsmndd  14171  prdsinvlem  14173  rhmf1o  14448  rnrhmsubrg  14533  rrgsupp  14547  psrbagfsupp  14978  psrbaglesuppg  14980  psrbaglesupp  14981  psrbaglecl  14983  psrbagcon  14985  psrbagconf1o  14987  mplsubgfilemcl  15013  cnrest2  15260  lmss  15270  lmtopcnp  15274  upxp  15296  uptx  15298  cnmpt11  15307  cnmpt21  15315  cnmpt22f  15319  cnmptcom  15322  hmeof1o2  15332  psmetxrge0  15356  isxmet2d  15372  blelrnps  15443  blelrn  15444  xmetresbl  15464  comet  15523  bdxmet  15525  xmettx  15534  dvidlemap  15715  dvidrelem  15716  dvidsslem  15717  dvaddxxbr  15725  dvmulxxbr  15726  dvrecap  15737  plyaddlem1  15771  upgredg  16299  vtxedgfi  16444  vtxlpfi  16445  depindlem2  16662  depindlem3  16663  nninfall  16957  nninfsellemeqinf  16964  nninffeq  16968  nnnninfex  16970  nninfnfiinf  16971  refeq  16978