Theorem ffnd 5426

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

Syntax hints:   -> wi 4   Fn wfn 5266   -->wf 5267

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 5275

This theorem is referenced by:  offeq  6172  caofid0l  6185  caofid0r  6186  caofid1  6187  caofid2  6188  difinfsn  7202  ctssdc  7215  nnnninfeq  7230  nninfdcinf  7273  nninfwlporlemd  7274  nninfwlporlem  7275  ofnegsub  9035  seqvalcd  10606  seq3feq2  10621  seq3feq  10625  seqf1oglem2  10665  seqfeq3  10674  ser0f  10679  facnn  10872  fac0  10873  resunimafz0  10976  wrdfn  11009  swrdvalfn  11109  seq3shft  11149  fisumss  11703  prodf1f  11854  efcvgfsum  11978  nninfctlemfo  12361  ennnfonelemfun  12788  ennnfonelemf1  12789  prdsplusgsgrpcl  13246  prdssgrpd  13247  prdsplusgcl  13278  prdsidlem  13279  prdsmndd  13280  mhmf1o  13302  resmhm2b  13321  mhmima  13323  mhmeql  13324  gsumwmhm  13330  grpinvf1o  13402  prdsinvlem  13440  ghmrn  13593  ghmpreima  13602  ghmeql  13603  ghmnsgima  13604  ghmnsgpreima  13605  ghmeqker  13607  ghmf1o  13611  gsumfzmptfidmadd  13675  rhmf1o  13930  rnrhmsubrg  14014  psrbaglesuppg  14434  mplsubgfilemcl  14461  cnrest2  14708  lmss  14718  lmtopcnp  14722  upxp  14744  uptx  14746  cnmpt11  14755  cnmpt21  14763  cnmpt22f  14767  cnmptcom  14770  hmeof1o2  14780  psmetxrge0  14804  isxmet2d  14820  blelrnps  14891  blelrn  14892  xmetresbl  14912  comet  14971  bdxmet  14973  xmettx  14982  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165  dvaddxxbr  15173  dvmulxxbr  15174  dvrecap  15185  plyaddlem1  15219  nninfall  15946  nninfsellemeqinf  15953  nninffeq  15957  nnnninfex  15959  nninfnfiinf  15960  refeq  15967