Theorem ffnd 5534

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

This proof depends on syntax axioms:   -> wi 4   Fn wfn 5372   -->wf 5373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-f 5381

This theorem is used by:  offeq  6316  caofid0l  6329  caofid0r  6330  caofid1  6331  caofid2  6332  fvdifsuppst  6484  suppsnopdc  6490  suppssdc  6500  suppssrst  6501  suppssrgst  6502  suppofss1dcl  6504  suppofss2dcl  6505  mapen  7146  difinfsn  7440  ctssdc  7453  nnnninfeq  7468  nninfdcinf  7511  nninfwlporlemd  7512  nninfwlporlem  7513  ofnegsub  9292  seqvalcd  10898  seq3feq2  10913  seq3feq  10917  seqf1oglem2  10957  seqfeq3  10966  ser0f  10971  facnn  11165  fac0  11166  resunimafz0  11274  wrdfn  11319  swrdvalfn  11428  pfxfn  11455  pfxid  11458  cats1un  11493  seq3shft  11603  fisumss  12159  prodf1f  12310  efcvgfsum  12434  nninfctlemfo  12817  ennnfonelemfun  13308  ennnfonelemf1  13309  mhmf1o  13777  resmhm2b  13796  mhmima  13798  mhmeql  13799  gzsumwmhm  13803  grpinvf1o  13875  ghmrn  14060  ghmpreima  14069  ghmeql  14070  ghmnsgima  14071  ghmnsgpreima  14072  ghmeqker  14074  ghmf1o  14078  gsumclfi  14159  gsumf1ofi  14160  gsumsubmclfi  14163  prdsplusgsgrpcl  14190  prdssgrpd  14191  prdsplusgcl  14192  prdsidlem  14193  prdsmndd  14194  prdsinvlem  14196  rhmf1o  14475  rnrhmsubrg  14560  rrgsupp  14574  psrbagfsupp  15055  psrbaglesuppg  15057  psrbaglesupp  15058  psrbaglecl  15060  psrbagcon  15062  psrbagconf1o  15064  mplsubgfilemcl  15090  cnrest2  15337  lmss  15347  lmtopcnp  15351  upxp  15373  uptx  15375  cnmpt11  15384  cnmpt21  15392  cnmpt22f  15396  cnmptcom  15399  hmeof1o2  15409  psmetxrge0  15433  isxmet2d  15449  blelrnps  15520  blelrn  15521  xmetresbl  15541  comet  15600  bdxmet  15602  xmettx  15611  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dvaddxxbr  15802  dvmulxxbr  15803  dvrecap  15814  plyaddlem1  15848  upgredg  16385  vtxedgfi  16530  vtxlpfi  16531  depindlem2  16748  depindlem3  16749  nninfall  17052  nninfsellemeqinf  17059  nninffeq  17063  nnnninfex  17065  nninfnfiinf  17066  refeq  17073