Theorem ffnd 5514

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

Syntax hints:   -> wi 4   Fn wfn 5352   -->wf 5353

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 5361

This theorem is referenced by:  offeq  6289  caofid0l  6302  caofid0r  6303  caofid1  6304  caofid2  6305  fvdifsuppst  6457  suppsnopdc  6463  suppssdc  6473  suppssrst  6474  suppssrgst  6475  suppofss1dcl  6477  suppofss2dcl  6478  mapen  7112  difinfsn  7404  ctssdc  7417  nnnninfeq  7432  nninfdcinf  7475  nninfwlporlemd  7476  nninfwlporlem  7477  ofnegsub  9253  seqvalcd  10847  seq3feq2  10862  seq3feq  10866  seqf1oglem2  10906  seqfeq3  10915  ser0f  10920  facnn  11114  fac0  11115  resunimafz0  11223  wrdfn  11264  swrdvalfn  11373  pfxfn  11400  pfxid  11403  cats1un  11438  seq3shft  11548  fisumss  12103  prodf1f  12254  efcvgfsum  12378  nninfctlemfo  12761  ennnfonelemfun  13252  ennnfonelemf1  13253  mhmf1o  13725  resmhm2b  13744  mhmima  13746  mhmeql  13747  gsumwmhm  13753  grpinvf1o  13825  ghmrn  14010  ghmpreima  14019  ghmeql  14020  ghmnsgima  14021  ghmnsgpreima  14022  ghmeqker  14024  ghmf1o  14028  gsumfzmptfidmadd  14092  gfsumcl  14110  prdsplusgsgrpcl  14132  prdssgrpd  14133  prdsplusgcl  14134  prdsidlem  14135  prdsmndd  14136  prdsinvlem  14138  rhmf1o  14413  rnrhmsubrg  14498  rrgsupp  14512  psrbagfsupp  14945  psrbaglesuppg  14947  psrbaglesupp  14948  psrbaglecl  14950  psrbagcon  14952  psrbagconf1o  14954  mplsubgfilemcl  14980  cnrest2  15227  lmss  15237  lmtopcnp  15241  upxp  15263  uptx  15265  cnmpt11  15274  cnmpt21  15282  cnmpt22f  15286  cnmptcom  15289  hmeof1o2  15299  psmetxrge0  15323  isxmet2d  15339  blelrnps  15410  blelrn  15411  xmetresbl  15431  comet  15490  bdxmet  15492  xmettx  15501  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvaddxxbr  15692  dvmulxxbr  15693  dvrecap  15704  plyaddlem1  15738  upgredg  16265  vtxedgfi  16410  vtxlpfi  16411  depindlem2  16628  depindlem3  16629  nninfall  16913  nninfsellemeqinf  16920  nninffeq  16924  nnnninfex  16926  nninfnfiinf  16927  refeq  16934