Theorem ffnd 5411

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

Syntax hints:   -> wi 4   Fn wfn 5254   -->wf 5255

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 5263

This theorem is referenced by:  offeq  6153  caofid0l  6166  caofid0r  6167  caofid1  6168  caofid2  6169  difinfsn  7175  ctssdc  7188  nnnninfeq  7203  nninfdcinf  7246  nninfwlporlemd  7247  nninfwlporlem  7248  ofnegsub  9006  seqvalcd  10570  seq3feq2  10585  seq3feq  10589  seqf1oglem2  10629  seqfeq3  10638  ser0f  10643  facnn  10836  fac0  10837  resunimafz0  10940  wrdfn  10967  seq3shft  11020  fisumss  11574  prodf1f  11725  efcvgfsum  11849  nninfctlemfo  12232  ennnfonelemfun  12659  ennnfonelemf1  12660  prdsplusgsgrpcl  13116  prdssgrpd  13117  prdsplusgcl  13148  prdsidlem  13149  prdsmndd  13150  mhmf1o  13172  resmhm2b  13191  mhmima  13193  mhmeql  13194  gsumwmhm  13200  grpinvf1o  13272  prdsinvlem  13310  ghmrn  13463  ghmpreima  13472  ghmeql  13473  ghmnsgima  13474  ghmnsgpreima  13475  ghmeqker  13477  ghmf1o  13481  gsumfzmptfidmadd  13545  rhmf1o  13800  rnrhmsubrg  13884  psrbaglesuppg  14302  cnrest2  14556  lmss  14566  lmtopcnp  14570  upxp  14592  uptx  14594  cnmpt11  14603  cnmpt21  14611  cnmpt22f  14615  cnmptcom  14618  hmeof1o2  14628  psmetxrge0  14652  isxmet2d  14668  blelrnps  14739  blelrn  14740  xmetresbl  14760  comet  14819  bdxmet  14821  xmettx  14830  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvaddxxbr  15021  dvmulxxbr  15022  dvrecap  15033  plyaddlem1  15067  nninfall  15740  nninfsellemeqinf  15747  nninffeq  15751  refeq  15759