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  6249  caofid0l  6262  caofid0r  6263  caofid1  6264  caofid2  6265  difinfsn  7299  ctssdc  7312  nnnninfeq  7327  nninfdcinf  7370  nninfwlporlemd  7371  nninfwlporlem  7372  ofnegsub  9142  seqvalcd  10724  seq3feq2  10739  seq3feq  10743  seqf1oglem2  10783  seqfeq3  10792  ser0f  10797  facnn  10990  fac0  10991  resunimafz0  11096  wrdfn  11132  swrdvalfn  11241  pfxfn  11268  pfxid  11271  cats1un  11306  seq3shft  11416  fisumss  11971  prodf1f  12122  efcvgfsum  12246  nninfctlemfo  12629  ennnfonelemfun  13056  ennnfonelemf1  13057  prdsplusgsgrpcl  13515  prdssgrpd  13516  prdsplusgcl  13547  prdsidlem  13548  prdsmndd  13549  mhmf1o  13571  resmhm2b  13590  mhmima  13592  mhmeql  13593  gsumwmhm  13599  grpinvf1o  13671  prdsinvlem  13709  ghmrn  13862  ghmpreima  13871  ghmeql  13872  ghmnsgima  13873  ghmnsgpreima  13874  ghmeqker  13876  ghmf1o  13880  gsumfzmptfidmadd  13944  rhmf1o  14201  rnrhmsubrg  14285  psrbaglesuppg  14705  mplsubgfilemcl  14732  cnrest2  14979  lmss  14989  lmtopcnp  14993  upxp  15015  uptx  15017  cnmpt11  15026  cnmpt21  15034  cnmpt22f  15038  cnmptcom  15041  hmeof1o2  15051  psmetxrge0  15075  isxmet2d  15091  blelrnps  15162  blelrn  15163  xmetresbl  15183  comet  15242  bdxmet  15244  xmettx  15253  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436  dvaddxxbr  15444  dvmulxxbr  15445  dvrecap  15456  plyaddlem1  15490  upgredg  16014  vtxedgfi  16159  vtxlpfi  16160  depindlem2  16377  depindlem3  16378  nninfall  16662  nninfsellemeqinf  16669  nninffeq  16673  nnnninfex  16675  nninfnfiinf  16676  refeq  16683  gfsumcl  16739