Theorem ffnd 5959

Description: A mapping is a function with domain, deduction form. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypothesis

Ref	Expression
ffnd.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
ffnd	⊢ (𝜑 → 𝐹 Fn 𝐴)

Proof of Theorem ffnd

Step	Hyp	Ref	Expression
1		ffnd.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		ffn 5958	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 5799  ⟶wf 5800

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 196  df-an 385  df-f 5808

This theorem is referenced by:  oprres  6700  isacs4lem  16991  gsumzaddlem  18144  ablfac1eu  18295  lmodfopnelem1  18722  psrbaglefi  19193  psrvscaval  19213  psrlidm  19224  psrridm  19225  psrass1  19226  psrdi  19227  psrdir  19228  mplsubglem  19255  mplvscaval  19269  mplbas2  19291  evlslem3  19335  evlslem1  19336  evlsvar  19344  ptbasfi  21194  rrxmet  22999  itg2cnlem2  23335  mdegldg  23630  fta1glem2  23730  fta1blem  23732  aannenlem1  23887  dchrisum0re  25002  ofpreima2  28849  matunitlindflem1  32575  mblfinlem2  32617  fsovf1od  37330  brcoffn  37348  clsneiel1  37426  ssmapsn  38403  fsumsupp0  38645  volicoff  38888  sge0resrn  39297  sge0le  39300  sge0fodjrnlem  39309  sge0seq  39339  nnfoctbdjlem  39348  meadjiunlem  39358  omeiunle  39407  hoicvr  39438  ovnovollem1  39546  ovnovollem2  39547  iinhoiicclem  39564  iunhoiioolem  39566  preimaicomnf  39599  smfresal  39673  resunimafz0  40368  vtxdgfisf  40691  2pthon3v-av  41150  amgmwlem  42357