Theorem ffnd 6046

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

Syntax hints:   -> wi 4   Fn wfn 5883   -->wf 5884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-f 5892

This theorem is referenced by:  fofn  6117  oprres  6802  fnwelem  7292  resunimafz0  13229  isacs4lem  17168  gsumzaddlem  18321  ablfac1eu  18472  lmodfopnelem1  18899  psrbaglefi  19372  psrvscaval  19392  psrlidm  19403  psrridm  19404  psrass1  19405  psrdi  19406  psrdir  19407  mplsubglem  19434  mplvscaval  19448  mplbas2  19470  evlslem3  19514  evlslem1  19515  evlsvar  19523  ptbasfi  21384  rrxmet  23191  itg2cnlem2  23529  mdegldg  23826  fta1glem2  23926  fta1blem  23928  aannenlem1  24083  dchrisum0re  25202  vtxdgfisf  26372  2pthon3v  26839  ofpreima2  29466  reprsuc  30693  circlemethhgt  30721  hgt750lemb  30734  matunitlindflem1  33405  mblfinlem2  33447  fsovf1od  38310  brcoffn  38328  clsneiel1  38406  ssmapsn  39408  preimaiocmnf  39788  fsumsupp0  39810  climinf2lem  39938  limsupmnflem  39952  limsupvaluz2  39970  supcnvlimsup  39972  limsupgtlem  40009  liminfvalxr  40015  liminflelimsupuz  40017  xlimconst2  40061  climxlim2  40072  volicoff  40212  sge0resrn  40621  sge0le  40624  sge0fodjrnlem  40633  sge0seq  40663  nnfoctbdjlem  40672  meadjiunlem  40682  omeiunle  40731  hoicvr  40762  ovnovollem1  40870  ovnovollem2  40871  iinhoiicclem  40887  iunhoiioolem  40889  preimaicomnf  40922  smfresal  40995  smfsuplem1  41017  smflimsuplem2  41027  amgmwlem  42548