Theorem ffnd 5474

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

Syntax hints:   -> wi 4   Fn wfn 5313   -->wf 5314

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 5322

This theorem is referenced by:  offeq  6238  caofid0l  6251  caofid0r  6252  caofid1  6253  caofid2  6254  difinfsn  7278  ctssdc  7291  nnnninfeq  7306  nninfdcinf  7349  nninfwlporlemd  7350  nninfwlporlem  7351  ofnegsub  9120  seqvalcd  10695  seq3feq2  10710  seq3feq  10714  seqf1oglem2  10754  seqfeq3  10763  ser0f  10768  facnn  10961  fac0  10962  resunimafz0  11066  wrdfn  11099  swrdvalfn  11204  pfxfn  11231  pfxid  11234  cats1un  11269  seq3shft  11365  fisumss  11919  prodf1f  12070  efcvgfsum  12194  nninfctlemfo  12577  ennnfonelemfun  13004  ennnfonelemf1  13005  prdsplusgsgrpcl  13463  prdssgrpd  13464  prdsplusgcl  13495  prdsidlem  13496  prdsmndd  13497  mhmf1o  13519  resmhm2b  13538  mhmima  13540  mhmeql  13541  gsumwmhm  13547  grpinvf1o  13619  prdsinvlem  13657  ghmrn  13810  ghmpreima  13819  ghmeql  13820  ghmnsgima  13821  ghmnsgpreima  13822  ghmeqker  13824  ghmf1o  13828  gsumfzmptfidmadd  13892  rhmf1o  14148  rnrhmsubrg  14232  psrbaglesuppg  14652  mplsubgfilemcl  14679  cnrest2  14926  lmss  14936  lmtopcnp  14940  upxp  14962  uptx  14964  cnmpt11  14973  cnmpt21  14981  cnmpt22f  14985  cnmptcom  14988  hmeof1o2  14998  psmetxrge0  15022  isxmet2d  15038  blelrnps  15109  blelrn  15110  xmetresbl  15130  comet  15189  bdxmet  15191  xmettx  15200  dvidlemap  15381  dvidrelem  15382  dvidsslem  15383  dvaddxxbr  15391  dvmulxxbr  15392  dvrecap  15403  plyaddlem1  15437  upgredg  15958  vtxedgfi  16049  vtxlpfi  16050  nninfall  16463  nninfsellemeqinf  16470  nninffeq  16474  nnnninfex  16476  nninfnfiinf  16477  refeq  16484