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  6232  caofid0l  6245  caofid0r  6246  caofid1  6247  caofid2  6248  difinfsn  7267  ctssdc  7280  nnnninfeq  7295  nninfdcinf  7338  nninfwlporlemd  7339  nninfwlporlem  7340  ofnegsub  9109  seqvalcd  10683  seq3feq2  10698  seq3feq  10702  seqf1oglem2  10742  seqfeq3  10751  ser0f  10756  facnn  10949  fac0  10950  resunimafz0  11053  wrdfn  11086  swrdvalfn  11188  pfxfn  11215  pfxid  11218  cats1un  11253  seq3shft  11349  fisumss  11903  prodf1f  12054  efcvgfsum  12178  nninfctlemfo  12561  ennnfonelemfun  12988  ennnfonelemf1  12989  prdsplusgsgrpcl  13447  prdssgrpd  13448  prdsplusgcl  13479  prdsidlem  13480  prdsmndd  13481  mhmf1o  13503  resmhm2b  13522  mhmima  13524  mhmeql  13525  gsumwmhm  13531  grpinvf1o  13603  prdsinvlem  13641  ghmrn  13794  ghmpreima  13803  ghmeql  13804  ghmnsgima  13805  ghmnsgpreima  13806  ghmeqker  13808  ghmf1o  13812  gsumfzmptfidmadd  13876  rhmf1o  14132  rnrhmsubrg  14216  psrbaglesuppg  14636  mplsubgfilemcl  14663  cnrest2  14910  lmss  14920  lmtopcnp  14924  upxp  14946  uptx  14948  cnmpt11  14957  cnmpt21  14965  cnmpt22f  14969  cnmptcom  14972  hmeof1o2  14982  psmetxrge0  15006  isxmet2d  15022  blelrnps  15093  blelrn  15094  xmetresbl  15114  comet  15173  bdxmet  15175  xmettx  15184  dvidlemap  15365  dvidrelem  15366  dvidsslem  15367  dvaddxxbr  15375  dvmulxxbr  15376  dvrecap  15387  plyaddlem1  15421  upgredg  15942  nninfall  16375  nninfsellemeqinf  16382  nninffeq  16386  nnnninfex  16388  nninfnfiinf  16389  refeq  16396