Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ffnd Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 ffnd.1 . 2 (𝜑𝐹:𝐴𝐵)
2 ffn 5958 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 17 1 (𝜑𝐹 Fn 𝐴)
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator