Theorem ffnd 5483

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

Syntax hints:   -> wi 4   Fn wfn 5321   -->wf 5322

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 5330

This theorem is referenced by:  offeq  6248  caofid0l  6261  caofid0r  6262  caofid1  6263  caofid2  6264  difinfsn  7298  ctssdc  7311  nnnninfeq  7326  nninfdcinf  7369  nninfwlporlemd  7370  nninfwlporlem  7371  ofnegsub  9141  seqvalcd  10722  seq3feq2  10737  seq3feq  10741  seqf1oglem2  10781  seqfeq3  10790  ser0f  10795  facnn  10988  fac0  10989  resunimafz0  11094  wrdfn  11127  swrdvalfn  11236  pfxfn  11263  pfxid  11266  cats1un  11301  seq3shft  11398  fisumss  11952  prodf1f  12103  efcvgfsum  12227  nninfctlemfo  12610  ennnfonelemfun  13037  ennnfonelemf1  13038  prdsplusgsgrpcl  13496  prdssgrpd  13497  prdsplusgcl  13528  prdsidlem  13529  prdsmndd  13530  mhmf1o  13552  resmhm2b  13571  mhmima  13573  mhmeql  13574  gsumwmhm  13580  grpinvf1o  13652  prdsinvlem  13690  ghmrn  13843  ghmpreima  13852  ghmeql  13853  ghmnsgima  13854  ghmnsgpreima  13855  ghmeqker  13857  ghmf1o  13861  gsumfzmptfidmadd  13925  rhmf1o  14181  rnrhmsubrg  14265  psrbaglesuppg  14685  mplsubgfilemcl  14712  cnrest2  14959  lmss  14969  lmtopcnp  14973  upxp  14995  uptx  14997  cnmpt11  15006  cnmpt21  15014  cnmpt22f  15018  cnmptcom  15021  hmeof1o2  15031  psmetxrge0  15055  isxmet2d  15071  blelrnps  15142  blelrn  15143  xmetresbl  15163  comet  15222  bdxmet  15224  xmettx  15233  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dvaddxxbr  15424  dvmulxxbr  15425  dvrecap  15436  plyaddlem1  15470  upgredg  15994  vtxedgfi  16139  vtxlpfi  16140  nninfall  16611  nninfsellemeqinf  16618  nninffeq  16622  nnnninfex  16624  nninfnfiinf  16625  refeq  16632