Theorem ffnd 5480

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

Syntax hints:   -> wi 4   Fn wfn 5319   -->wf 5320

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 5328

This theorem is referenced by:  offeq  6244  caofid0l  6257  caofid0r  6258  caofid1  6259  caofid2  6260  difinfsn  7290  ctssdc  7303  nnnninfeq  7318  nninfdcinf  7361  nninfwlporlemd  7362  nninfwlporlem  7363  ofnegsub  9132  seqvalcd  10713  seq3feq2  10728  seq3feq  10732  seqf1oglem2  10772  seqfeq3  10781  ser0f  10786  facnn  10979  fac0  10980  resunimafz0  11085  wrdfn  11118  swrdvalfn  11227  pfxfn  11254  pfxid  11257  cats1un  11292  seq3shft  11389  fisumss  11943  prodf1f  12094  efcvgfsum  12218  nninfctlemfo  12601  ennnfonelemfun  13028  ennnfonelemf1  13029  prdsplusgsgrpcl  13487  prdssgrpd  13488  prdsplusgcl  13519  prdsidlem  13520  prdsmndd  13521  mhmf1o  13543  resmhm2b  13562  mhmima  13564  mhmeql  13565  gsumwmhm  13571  grpinvf1o  13643  prdsinvlem  13681  ghmrn  13834  ghmpreima  13843  ghmeql  13844  ghmnsgima  13845  ghmnsgpreima  13846  ghmeqker  13848  ghmf1o  13852  gsumfzmptfidmadd  13916  rhmf1o  14172  rnrhmsubrg  14256  psrbaglesuppg  14676  mplsubgfilemcl  14703  cnrest2  14950  lmss  14960  lmtopcnp  14964  upxp  14986  uptx  14988  cnmpt11  14997  cnmpt21  15005  cnmpt22f  15009  cnmptcom  15012  hmeof1o2  15022  psmetxrge0  15046  isxmet2d  15062  blelrnps  15133  blelrn  15134  xmetresbl  15154  comet  15213  bdxmet  15215  xmettx  15224  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvaddxxbr  15415  dvmulxxbr  15416  dvrecap  15427  plyaddlem1  15461  upgredg  15983  vtxedgfi  16095  vtxlpfi  16096  nninfall  16547  nninfsellemeqinf  16554  nninffeq  16558  nnnninfex  16560  nninfnfiinf  16561  refeq  16568