Theorem ffnd 5509

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

Syntax hints:   -> wi 4   Fn wfn 5347   -->wf 5348

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 5356

This theorem is referenced by:  offeq  6280  caofid0l  6293  caofid0r  6294  caofid1  6295  caofid2  6296  fvdifsuppst  6444  suppsnopdc  6450  suppssdc  6460  suppssrst  6461  suppssrgst  6462  suppofss1dcl  6464  suppofss2dcl  6465  mapen  7099  difinfsn  7391  ctssdc  7404  nnnninfeq  7419  nninfdcinf  7462  nninfwlporlemd  7463  nninfwlporlem  7464  ofnegsub  9236  seqvalcd  10823  seq3feq2  10838  seq3feq  10842  seqf1oglem2  10882  seqfeq3  10891  ser0f  10896  facnn  11089  fac0  11090  resunimafz0  11198  wrdfn  11239  swrdvalfn  11348  pfxfn  11375  pfxid  11378  cats1un  11413  seq3shft  11523  fisumss  12078  prodf1f  12229  efcvgfsum  12353  nninfctlemfo  12736  ennnfonelemfun  13168  ennnfonelemf1  13169  prdsplusgsgrpcl  13627  prdssgrpd  13628  prdsplusgcl  13659  prdsidlem  13660  prdsmndd  13661  mhmf1o  13683  resmhm2b  13702  mhmima  13704  mhmeql  13705  gsumwmhm  13711  grpinvf1o  13783  prdsinvlem  13821  ghmrn  13974  ghmpreima  13983  ghmeql  13984  ghmnsgima  13985  ghmnsgpreima  13986  ghmeqker  13988  ghmf1o  13992  gsumfzmptfidmadd  14056  rhmf1o  14313  rnrhmsubrg  14397  rrgsupp  14411  psrbagfsupp  14819  psrbaglesuppg  14821  psrbaglesupp  14822  psrbaglecl  14824  psrbagcon  14826  psrbagconf1o  14828  mplsubgfilemcl  14854  cnrest2  15101  lmss  15111  lmtopcnp  15115  upxp  15137  uptx  15139  cnmpt11  15148  cnmpt21  15156  cnmpt22f  15160  cnmptcom  15163  hmeof1o2  15173  psmetxrge0  15197  isxmet2d  15213  blelrnps  15284  blelrn  15285  xmetresbl  15305  comet  15364  bdxmet  15366  xmettx  15375  dvidlemap  15556  dvidrelem  15557  dvidsslem  15558  dvaddxxbr  15566  dvmulxxbr  15567  dvrecap  15578  plyaddlem1  15612  upgredg  16139  vtxedgfi  16284  vtxlpfi  16285  depindlem2  16502  depindlem3  16503  nninfall  16787  nninfsellemeqinf  16794  nninffeq  16798  nnnninfex  16800  nninfnfiinf  16801  refeq  16808  gfsumcl  16870