Theorem ffnd 5537

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 5536	. 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 5375   -->wf 5376

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 5384

This theorem is used by:  offeq  6320  caofid0l  6333  caofid0r  6334  caofid1  6335  caofid2  6336  fvdifsuppst  6488  suppsnopdc  6494  suppssdc  6504  suppssrst  6505  suppssrgst  6506  suppofss1dcl  6508  suppofss2dcl  6509  suppinisegdc  6513  mapen  7152  funisfsuppdc  7298  difinfsn  7446  ctssdc  7459  nnnninfeq  7474  nninfdcinf  7517  nninfwlporlemd  7518  nninfwlporlem  7519  ofsubeq0  9300  ofnegsub  9301  seqvalcd  10918  seq3feq2  10933  seq3feq  10937  seqf1oglem2  10977  seqfeq3  10986  ser0f  10991  facnn  11186  fac0  11187  resunimafz0  11295  wrdfn  11340  swrdvalfn  11449  pfxfn  11476  pfxid  11479  cats1un  11514  seq3shft  11624  fisumss  12183  prodf1f  12334  efcvgfsum  12458  nninfctlemfo  12841  ennnfonelemfun  13365  ennnfonelemf1  13366  mhmf1o  13835  resmhm2b  13854  mhmima  13856  mhmeql  13857  gzsumwmhm  13861  grpinvf1o  13933  ghmrn  14118  ghmpreima  14127  ghmeql  14128  ghmnsgima  14129  ghmnsgpreima  14130  ghmeqker  14132  ghmf1o  14136  cntzmhm  14172  gsumclfi  14248  gsumf1ofi  14249  gsumsubmclfi  14252  prdsplusgsgrpcl  14296  prdssgrpd  14297  prdsplusgcl  14298  prdsidlem  14299  prdsmndd  14300  prdsinvlem  14302  rhmf1o  14583  rnrhmsubrg  14668  rrgsupp  14682  psrbaglesuppg  15170  psrbaglesupp  15171  psrbaglecl  15172  psrbagcon  15174  psrbaglefifi  15175  psrbagconf1o  15177  psrbagmaxlem1x  15181  psrbagmaxlem1y  15182  gsumbagdiaglem  15184  psrass1filem  15186  psrlidmfi  15208  psrridmfi  15209  psrass1fi  15210  psrdifi  15211  psrdirfi  15212  mplsubgfilemcl  15232  mplsubgfileminv  15233  cnrest2  15479  lmss  15489  lmtopcnp  15493  upxp  15515  uptx  15517  cnmpt11  15526  cnmpt21  15534  cnmpt22f  15538  cnmptcom  15541  hmeof1o2  15551  psmetxrge0  15575  isxmet2d  15591  blelrnps  15662  blelrn  15663  xmetresbl  15683  comet  15742  bdxmet  15744  xmettx  15753  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvaddxxbr  15944  dvmulxxbr  15945  dvrecap  15956  plyaddlem1  15990  upgredg  16607  vtxedgfi  16752  vtxlpfi  16753  depindlem2  16970  depindlem3  16971  nninfall  17275  nninfsellemeqinf  17282  nninffeq  17286  nnnninfex  17288  nninfnfiinf  17289  refeq  17296