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

Theorem ffnd 6084
 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 6083 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 17 1 (𝜑𝐹 Fn 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   Fn wfn 5921  ⟶wf 5922 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 385  df-f 5930 This theorem is referenced by:  fofn  6155  oprres  6844  fnwelem  7337  resunimafz0  13267  cats1un  13521  isacs4lem  17215  gsumzaddlem  18367  ablfac1eu  18518  lmodfopnelem1  18947  psrbaglefi  19420  psrvscaval  19440  psrlidm  19451  psrridm  19452  psrass1  19453  psrdi  19454  psrdir  19455  mplsubglem  19482  mplvscaval  19496  mplbas2  19518  evlslem3  19562  evlslem1  19563  evlsvar  19571  ptbasfi  21432  rrxmet  23237  itg2cnlem2  23574  mdegldg  23871  fta1glem2  23971  fta1blem  23973  aannenlem1  24128  dchrisum0re  25247  vtxdgfisf  26428  2pthon3v  26908  ofpreima2  29594  reprsuc  30821  circlemethhgt  30849  hgt750lemb  30862  matunitlindflem1  33535  mblfinlem2  33577  fsovf1od  38627  brcoffn  38645  clsneiel1  38723  ssmapsn  39722  preimaiocmnf  40106  fsumsupp0  40128  climinf2lem  40256  limsupmnflem  40270  limsupvaluz2  40288  supcnvlimsup  40290  limsupgtlem  40327  liminfvalxr  40333  liminflelimsupuz  40335  xlimconst2  40379  climxlim2  40390  volicoff  40530  sge0resrn  40939  sge0le  40942  sge0fodjrnlem  40951  sge0seq  40981  nnfoctbdjlem  40990  meadjiunlem  41000  omeiunle  41052  hoicvr  41083  ovnovollem1  41191  ovnovollem2  41192  iinhoiicclem  41208  iunhoiioolem  41210  preimaicomnf  41243  smfresal  41316  smfsuplem1  41338  smflimsuplem2  41348  amgmwlem  42876
 Copyright terms: Public domain W3C validator