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

Theorem ffnd 5945
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 5944 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 17 1 (𝜑𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 5785  wf 5786
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 195  df-an 384  df-f 5794
This theorem is referenced by:  isacs4lem  16937  gsumzaddlem  18090  ablfac1eu  18241  lmodfopnelem1  18668  psrbaglefi  19139  psrvscaval  19159  psrlidm  19170  psrridm  19171  psrass1  19172  psrdi  19173  psrdir  19174  mplsubglem  19201  mplvscaval  19215  mplbas2  19237  evlslem3  19281  evlslem1  19282  evlsvar  19290  ptbasfi  21136  rrxmet  22916  itg2cnlem2  23252  mdegldg  23547  fta1glem2  23647  fta1blem  23649  aannenlem1  23804  dchrisum0re  24919  ofpreima2  28655  matunitlindflem1  32371  mblfinlem2  32413  fsovf1od  37126  brcoffn  37144  clsneiel1  37222  ssmapsn  38199  fsumsupp0  38442  volicoff  38685  sge0resrn  39094  sge0le  39097  sge0fodjrnlem  39106  sge0seq  39136  nnfoctbdjlem  39145  meadjiunlem  39155  omeiunle  39204  hoicvr  39235  ovnovollem1  39343  ovnovollem2  39344  iinhoiicclem  39361  iunhoiioolem  39363  preimaicomnf  39396  smfresal  39470  resunimafz0  40188  vtxdgfisf  40686  2pthon3v-av  41145  amgmwlem  42313
  Copyright terms: Public domain W3C validator