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  mapen  7150  difinfsn  7446  ctssdc  7459  nnnninfeq  7474  nninfdcinf  7517  nninfwlporlemd  7518  nninfwlporlem  7519  ofsubeq0  9300  ofnegsub  9301  seqvalcd  10919  seq3feq2  10934  seq3feq  10938  seqf1oglem2  10978  seqfeq3  10987  ser0f  10992  facnn  11187  fac0  11188  resunimafz0  11296  wrdfn  11341  swrdvalfn  11450  pfxfn  11477  pfxid  11480  cats1un  11515  seq3shft  11625  fisumss  12184  prodf1f  12335  efcvgfsum  12459  nninfctlemfo  12842  ennnfonelemfun  13366  ennnfonelemf1  13367  mhmf1o  13836  resmhm2b  13855  mhmima  13857  mhmeql  13858  gzsumwmhm  13862  grpinvf1o  13934  ghmrn  14119  ghmpreima  14128  ghmeql  14129  ghmnsgima  14130  ghmnsgpreima  14131  ghmeqker  14133  ghmf1o  14137  cntzmhm  14173  gsumclfi  14249  gsumf1ofi  14250  gsumsubmclfi  14253  prdsplusgsgrpcl  14297  prdssgrpd  14298  prdsplusgcl  14299  prdsidlem  14300  prdsmndd  14301  prdsinvlem  14303  rhmf1o  14584  rnrhmsubrg  14669  rrgsupp  14683  psrbagfsupp  15164  psrbaglesuppg  15166  psrbaglesupp  15167  psrbaglecl  15169  psrbagcon  15171  psrbaglefifi  15172  psrbagconf1o  15174  gsumbagdiaglem  15175  psrass1filem  15177  psrlidmfi  15199  psrridmfi  15200  psrass1fi  15201  psrdifi  15202  psrdirfi  15203  mplsubgfilemcl  15215  cnrest2  15462  lmss  15472  lmtopcnp  15476  upxp  15498  uptx  15500  cnmpt11  15509  cnmpt21  15517  cnmpt22f  15521  cnmptcom  15524  hmeof1o2  15534  psmetxrge0  15558  isxmet2d  15574  blelrnps  15645  blelrn  15646  xmetresbl  15666  comet  15725  bdxmet  15727  xmettx  15736  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dvaddxxbr  15927  dvmulxxbr  15928  dvrecap  15939  plyaddlem1  15973  upgredg  16590  vtxedgfi  16735  vtxlpfi  16736  depindlem2  16953  depindlem3  16954  nninfall  17258  nninfsellemeqinf  17265  nninffeq  17269  nnnninfex  17271  nninfnfiinf  17272  refeq  17279